discouraged updated, syl5eq replaced by eqtrid

discouraged

@@ -5036,7 +5036,6 @@
 "df-rngo" is used by "relrngo".
 "df-rq" is used by "dmrecnq".
 "df-rq" is used by "recmulnq".
-"df-sca" is used by "bj-isrvec".
 "df-sca" is used by "mgpscaOLD".
 "df-sca" is used by "mnringscadOLD".
 "df-sca" is used by "opsrscaOLD".
@@ -15701,7 +15700,7 @@ New usage of "df-ringcALTV" is discouraged (1 uses).
 New usage of "df-rngcALTV" is discouraged (1 uses).
 New usage of "df-rngo" is discouraged (2 uses).
 New usage of "df-rq" is discouraged (2 uses).
-New usage of "df-sca" is discouraged (7 uses).
+New usage of "df-sca" is discouraged (6 uses).
 New usage of "df-setrecs" is discouraged (5 uses).
 New usage of "df-sgrOLD" is discouraged (2 uses).
 New usage of "df-sh" is discouraged (1 uses).

set.mm

@@ -200003,7 +200003,7 @@ class of all (base sets of) groups is proper.  (Contributed by Mario
        extractors ` E ` at a proper class.  Extracted from several former
        proofs of lemmas like ~ zlmlem .  (Contributed by AV, 31-Oct-2024.) $)
     fveqprc $p |- ( -. X e. _V -> ( E ` X ) = ( E ` Y ) ) $=
-      ( cvv wcel wn c0 cfv eqcomi fvprc syl5eq fveq2d 3eqtr4a ) CGHIZJJAKZCAKDA
+      ( cvv wcel wn c0 cfv eqcomi fvprc eqtrid fveq2d 3eqtr4a ) CGHIZJJAKZCAKDA
       KRJELCAMQDJAQDCBKJFCBMNOP $.
   $}
 
@@ -200015,7 +200015,7 @@ class of all (base sets of) groups is proper.  (Contributed by Mario
        extractors ` E ` at a proper class.  Extracted from several former
        proofs of lemmas like ~ resvlem .  (Contributed by AV, 31-Oct-2024.) $)
     oveqprc $p |- ( -. X e. _V -> ( E ` X ) = ( E ` Z ) ) $=
-      ( cvv wcel wn c0 cfv eqcomi fvprc co ovprc1 syl5eq fveq2d 3eqtr4a ) CIJKZ
+      ( cvv wcel wn c0 cfv eqcomi fvprc co ovprc1 eqtrid fveq2d 3eqtr4a ) CIJKZ
       LLAMZCAMEAMUBLFNCAOUAELAUAECDBPLGCDBHQRST $.
   $}
 
@@ -200593,7 +200593,7 @@ C_ dom ( S sSet <. I , E >. ) ) $=
     ressbas $p |- ( A e. V -> ( A i^i B ) = ( Base ` R ) ) $=
       ( cvv wcel cin cbs cfv wceq wss w3a fveq2d 3eqtr4a 3expib wn c0 wa wi cnx
       simp1 sseqin2 sylib ressid2 cop csts co simp2 fvexi baseid setsid sylancl
-      inex2 eqtr4d pm2.61i in0 fvprc syl5eq ineq2d cress base0 eqcomi reldmress
+      inex2 eqtr4d pm2.61i in0 fvprc eqtrid ineq2d cress base0 eqcomi reldmress
       ressval2 oveqprc eqtrd adantr pm2.61ian ) EHIZADIZABJZCKLZMZBANZVLVMUAVPU
       BVQVLVMVPVQVLVMOZBEKLZVNVOGVRVQVNBMVQVLVMUDBAUEUFVRCEKABCEHDFGUGPQRVQSZVL
       VMVPVTVLVMOZVNEUCKLVNUHUIUJZKLZVOWAVLVNHIVNWCMVTVLVMUKBABEKGULUPHVNKHEUMU
@@ -232745,7 +232745,7 @@ operation is a permutation group (group consisting of permutations), see
     symgvalstructOLD $p |- ( A e. V -> G = { <. ( Base ` ndx ) , B >. ,
         <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } ) $=
       ( wcel cfv wceq c0 cvv chash cc0 c1 clt wbr w3o cnx cbs cplusg hashv01gt1
-      cop cts ctp hasheq0 cefmnd csymg 0symgefmndeq eqcomi fveq2 syl5eq 3eqtr4a
+      cop cts ctp hasheq0 cefmnd csymg 0symgefmndeq eqcomi fveq2 eqtrid 3eqtr4a
       wa adantl eqid efmnd adantr cmap co csn 0map0sn0 id oveq12d cv cab fveq2d
       wf1o symgbas symgbas0 3eqtr3g opeq2d tpeq1d 3eqtrd ex sylbid wex hash1snb
       snex eleq1 mpbiri syl snsymgefmndeq eqtr4di eqtr4i 3eqtr3d exlimiv syl6bi