janitorial stuff (#4680)

* janitorial stuff

* update changes-set.txt

changes-set.txt

@@ -85,6 +85,7 @@ make a github issue.)
 
 DONE:
 Date      Old       New         Notes
+27-Feb-25 elnelall  pm2.24nel
 24-Feb-25 naddid1   naddrid
 24-Feb-25 naddid2   naddlid
 24-Feb-25 mulid1    mulrid

set.mm

@@ -28113,6 +28113,15 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
       ( wne wceq adantl pm2.61dane pm2.61ine ) ABDGBDIZACECEJANHKFLM $.
   $}
 
+  ${
+    mteqand.1 $e |- ( ph -> C =/= D ) $.
+    mteqand.2 $e |- ( ( ph /\ A = B ) -> C = D ) $.
+    $( A modus tollens deduction for inequality.  (Contributed by Steven
+       Nguyen, 1-Jun-2023.) $)
+    mteqand $p |- ( ph -> A =/= B ) $=
+      ( wceq neneqd mtand neqned ) ABCABCHDEHADEFIGJK $.
+  $}
+
   $( Logical OR with an equality.  (Contributed by NM, 29-Apr-2007.) $)
   neor $p |- ( ( A = B \/ ps ) <-> ( A =/= B -> ps ) ) $=
     ( wceq wo wn wi wne df-or df-ne imbi1i bitr4i ) BCDZAEMFZAGBCHZAGMAIONABCJK
@@ -28193,15 +28202,6 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
     xor3 ) ACDZBCDZESTFZGABGHZCIZSTJABHZCKZUCUAUEGUDGZCIUCUDCLUFUBCABRMNABCOPQ
     $.
 
-  ${
-    mteqand.1 $e |- ( ph -> C =/= D ) $.
-    mteqand.2 $e |- ( ( ph /\ A = B ) -> C = D ) $.
-    $( A modus tollens deduction for inequality.  (Contributed by Steven
-       Nguyen, 1-Jun-2023.) $)
-    mteqand $p |- ( ph -> A =/= B ) $=
-      ( wceq neneqd mtand neqned ) ABCABCHDEHADEFIGJK $.
-  $}
-
 
 $(
 -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
@@ -28233,6 +28233,14 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
       ( wnel wcel wn df-nel mpbir ) ABDABEFCABGH $.
   $}
 
+  ${
+    nelcon3d.1 $e |- ( ph -> ( A e. B -> C e. D ) ) $.
+    $( Contrapositive law deduction for negated membership.  (Contributed by
+       AV, 28-Jan-2020.) $)
+    nelcon3d $p |- ( ph -> ( C e/ D -> A e/ B ) ) $=
+      ( wcel wn wnel con3d df-nel 3imtr4g ) ADEGZHBCGZHDEIBCIANMFJDEKBCKL $.
+  $}
+
   ${
     neleq12d.1 $e |- ( ph -> A = B ) $.
     neleq12d.2 $e |- ( ph -> C = D ) $.
@@ -28289,17 +28297,9 @@ atomic formula (class version of ~ elsb1 ).  Usage of this theorem is
   elnelne2 $p |- ( ( A e. C /\ B e/ C ) -> A =/= B ) $=
     ( wnel wcel wn wne df-nel nelne2 sylan2b ) BCDACEBCEFABGBCHABCIJ $.
 
-  ${
-    nelcon3d.1 $e |- ( ph -> ( A e. B -> C e. D ) ) $.
-    $( Contrapositive law deduction for negated membership.  (Contributed by
-       AV, 28-Jan-2020.) $)
-    nelcon3d $p |- ( ph -> ( C e/ D -> A e/ B ) ) $=
-      ( wcel wn wnel con3d df-nel 3imtr4g ) ADEGZHBCGZHDEIBCIANMFJDEKBCKL $.
-  $}
-
   $( A contradiction concerning membership implies anything.  (Contributed by
      Alexander van der Vekens, 25-Jan-2018.) $)
-  elnelall $p |- ( A e. B -> ( A e/ B -> ph ) ) $=
+  pm2.24nel $p |- ( A e. B -> ( A e/ B -> ph ) ) $=
     ( wnel wcel wn df-nel pm2.24 biimtrid ) BCDBCEZFJABCGJAHI $.
 
   ${
@@ -144148,11 +144148,11 @@ Infinity and the extended real number system (cont.)
      24-Nov-2021.) $)
   xnn0lenn0nn0 $p |- ( ( M e. NN0* /\ N e. NN0 /\ M <_ N ) -> M e. NN0 ) $=
     ( cxnn0 wcel cn0 cle wbr cpnf wo wi elxnn0 2a1 wa wb breq1 nn0re syl sylbid
-    wceq cr adantr cxr rexrd xgepnf wnel pnfnre eleq1 syl6bi com13 ax-mp adantl
-    elnelall ex jaoi sylbi 3imp ) ACDZBEDZABFGZAEDZUQUTAHSZIURUSUTJZJZAKUTVCVAU
-    TURUSLVAURVBVAURMUSHBFGZUTVAUSVDNURAHBFOUAURVDUTJVAURVDBHSZUTURBUBDVDVENURB
-    BPUCBUDQHTUEZURVEUTJJUFVEURVFUTVEURHEDZVFUTJZBHEUGVGHTDVHHPUTHTULQUHUIUJRUK
-    RUMUNUOUP $.
+    wceq cr adantr rexrd xgepnf wnel pnfnre eleq1 pm2.24nel syl6bi com13 adantl
+    cxr ax-mp ex jaoi sylbi 3imp ) ACDZBEDZABFGZAEDZUQUTAHSZIURUSUTJZJZAKUTVCVA
+    UTURUSLVAURVBVAURMUSHBFGZUTVAUSVDNURAHBFOUAURVDUTJVAURVDBHSZUTURBUKDVDVENUR
+    BBPUBBUCQHTUDZURVEUTJJUEVEURVFUTVEURHEDZVFUTJZBHEUFVGHTDVHHPUTHTUGQUHUIULRU
+    JRUMUNUOUP $.
 
   $( An extended nonnegative integer which is less than or equal to 2 is either
      0 or 1 or 2.  (Contributed by AV, 24-Nov-2021.) $)
@@ -194572,15 +194572,15 @@ being prime ( ` Prime = { p e. NN | ... ` ), but even if ` p e. NN0 ` was
     ( c2 wcel cprime wnel c4 c1 clt wbr wa wi cz cle a1i caddc co wb sylancr c3
     sylbid cuz cfv cn eluz2b2 w3a 4z nnz ad2antrr 1z zltp1le breq1i bitrdi wceq
     1p1e2 wo cr 2re nnre leloe 2p1e3 3re df-4 biimpa eqbrtrid a1d neleq1 eqcoms
-    2z 3z ex 3prm elnelall mp1i jaod 2prm imp 3jca eluz2 syl6ibr sylbi ) ABUAUB
-    CZADEZAFUAUBCZWAAUCCZGAHIZJZWBWCKAUDWFWBFLCZALCZFAMIZUEZWCWFWBWJWFWBJZWGWHW
-    IWGWKUFNWDWHWEWBAUGZUHWFWBWIWDWEWBWIKZWDWEBAMIZWMWDWEGGOPZAMIZWNWDGLCWHWEWP
-    QUIWLGAUJRWOBAMUNUKULWDWNBAHIZBAUMZUOZWMWDBUPCAUPCZWNWSQUQAURZBAUSRWDWQWMWR
-    WDWQSAMIZWMWDWQBGOPZAMIZXBWDBLCWHWQXDQVHWLBAUJRXCSAMUTUKULWDXBSAHIZSAUMZUOZ
-    WMWDSUPCWTXBXGQVAXASAUSRWDXEWMXFWDXEWMWDXEJZWIWBXHFSGOPZAMVBWDXEXIAMIZWDSLC
-    WHXEXJQVIWLSAUJRVCVDVEVJXFWMKWDXFWBSDEZWIWBXKQASASDVFVGSDCXKWIKXFVKWISDVLVM
-    TNVNTTWRWMKWDWRWBBDEZWIWBXLQABABDVFVGBDCXLWIKWRVOWIBDVLVMTNVNTTVPVPVQVJFAVR
-    VSVTVP $.
+    2z 3z ex 3prm pm2.24nel mp1i jaod 2prm imp 3jca eluz2 syl6ibr sylbi ) ABUAU
+    BCZADEZAFUAUBCZWAAUCCZGAHIZJZWBWCKAUDWFWBFLCZALCZFAMIZUEZWCWFWBWJWFWBJZWGWH
+    WIWGWKUFNWDWHWEWBAUGZUHWFWBWIWDWEWBWIKZWDWEBAMIZWMWDWEGGOPZAMIZWNWDGLCWHWEW
+    PQUIWLGAUJRWOBAMUNUKULWDWNBAHIZBAUMZUOZWMWDBUPCAUPCZWNWSQUQAURZBAUSRWDWQWMW
+    RWDWQSAMIZWMWDWQBGOPZAMIZXBWDBLCWHWQXDQVHWLBAUJRXCSAMUTUKULWDXBSAHIZSAUMZUO
+    ZWMWDSUPCWTXBXGQVAXASAUSRWDXEWMXFWDXEWMWDXEJZWIWBXHFSGOPZAMVBWDXEXIAMIZWDSL
+    CWHXEXJQVIWLSAUJRVCVDVEVJXFWMKWDXFWBSDEZWIWBXKQASASDVFVGSDCXKWIKXFVKWISDVLV
+    MTNVNTTWRWMKWDWRWBBDEZWIWBXLQABABDVFVGBDCXLWIKWRVOWIBDVLVMTNVNTTVPVPVQVJFAV
+    RVSVTVP $.
 
   $( A square is never prime.  (Contributed by Mario Carneiro, 20-Jun-2015.) $)
   sqnprm $p |- ( A e. ZZ -> -. ( A ^ 2 ) e. Prime ) $=
@@ -772380,12 +772380,12 @@ known as function application (and called "alternate function value" in
                      -> ( ( ( F '''' A ) = B \/ ( F '''' A ) e/ ran F )
                       <-> ( ( F '''' A ) = B \/_ ( F '''' A ) e/ ran F ) ) ) $=
     ( crn wcel cafv2 wceq wnel wo wxo wn wi wa wb eleq1 eqcoms a1d jca ex com12
-    biimpa nnel sylibr anbi2d elnelall impcom syl6bir pm2.24 adantr jaoi df-xor
-    simpl xor3 dfbi2 3bitri syl6ibr xoror impbid1 ) BCDZEZACFZBGZVAUSHZIZVBVCJZ
-    UTVDVBVCKZLZVFVBLZMZVEVDUTVIVBUTVILVCVBUTVIVBUTMZVGVHVJVFVBVJVAUSEZVFVBUTVK
-    UTVKNBVABVAUSOPUAVAUSUBUCQVJVBVFVBUTULQRSVCUTVIVCUTMZVGVHVBVLVFVBVLVCVKMVFV
-    BVKUTVCVABUSOUDVKVCVFVFVAUSUEUFUGTVCVHUTVCVBUHUIRSUJTVEVBVCNKVBVFNVIVBVCUKV
-    BVCUMVBVFUNUOUPVBVCUQUR $.
+    biimpa nnel sylibr simpl anbi2d pm2.24nel impcom syl6bir pm2.24 adantr jaoi
+    df-xor xor3 dfbi2 3bitri syl6ibr xoror impbid1 ) BCDZEZACFZBGZVAUSHZIZVBVCJ
+    ZUTVDVBVCKZLZVFVBLZMZVEVDUTVIVBUTVILVCVBUTVIVBUTMZVGVHVJVFVBVJVAUSEZVFVBUTV
+    KUTVKNBVABVAUSOPUAVAUSUBUCQVJVBVFVBUTUDQRSVCUTVIVCUTMZVGVHVBVLVFVBVLVCVKMVF
+    VBVKUTVCVABUSOUEVKVCVFVFVAUSUFUGUHTVCVHUTVCVBUIUJRSUKTVEVBVCNKVBVFNVIVBVCUL
+    VBVCUMVBVFUNUOUPVBVCUQUR $.
 
   $( The alternate function value at a class ` A ` is defined, i.e., in the
      range of the function, iff ` A ` is in the domain of the function.