Merge branch 'develop' of https://github.com/metamath/set.mm into av-…

…fset3

big-unifier.mm

@@ -89,7 +89,7 @@ Dwight Megill (1950--2021).  For more information, visit
 
   $( A three-step proof that applies ~ ax-mp to the two axioms.  The proof was
      saved in compressed format with "SAVE PROOF theorem1 / COMPRESSED" in the
-     Metamath program. $)
+     Metamath program.  (Contributed by NM, 30-Aug-2008.) $)
   theorem1 $p |- e ( e ( e ( x , e ( y , e ( e ( e ( y , z ) , e ( u , z ) )
     , u ) ) ) , v ) , e ( x , v ) ) $=
     ( wi ax-min ax-maj ax-mp ) ABBCFECFFEFFZFZKDFADFFZAFZFJMFFZKNJFFNFZFAOFFZMP
@@ -98,7 +98,7 @@ Dwight Megill (1950--2021).  For more information, visit
   $( This is the same as ~ theorem1 , except that the proof is saved in
      uncompressed format with "SAVE PROOF theorem1u / NORMAL" in the Metamath
      program.  Note the size difference in the compressed versus uncompressed
-     proofs. $)
+     proofs.  (Contributed by NM, 30-Aug-2008.) $)
   theorem1u $p |- e ( e ( e ( x , e ( y , e ( e ( e ( y , z ) , e ( u , z ) )
     , u ) ) ) , v ) , e ( x , v ) ) $=
     wx wy wy wz wi wu wz wi wi wu wi wi wi wx wy wy wz wi wu wz wi wi wu wi wi

changes-set.txt

@@ -98,6 +98,7 @@ make a github issue.)
 
 DONE:
 Date      Old       New         Notes
+21-Sep-24 sb56      sbalex      substitution expressed with 'al' or with 'ex'
 21-Sep-24 nanimn    dfnan2      mark as an alternative definition
 20-Sep-24 fco3      funcofd     moved from GS's mathbox to main set.mm
 20-Sep-24 freld     [same]      moved from GS's mathbox to main set.mm

demo0.mm

@@ -73,7 +73,7 @@ Dwight Megill (1950--2021).  For more information, visit
     mp $a |- Q $.
   $}
 
-  $( Prove a theorem. $)
+  $( Prove a theorem.  (Contributed by NM, 1-Jan-2004.) $)
   th1 $p |- t = t $=
   $( Here is its proof: $)
     tt tze tpl tt weq tt tt weq tt a2 tt tze tpl tt weq tt tze tpl tt weq tt tt

discouraged

@@ -13811,6 +13811,7 @@ New usage of "0reALT" is discouraged (0 uses).
 New usage of "0vfval" is discouraged (9 uses).
 New usage of "139prmALT" is discouraged (0 uses).
 New usage of "19.21a3con13vVD" is discouraged (0 uses).
+New usage of "19.36imvOLD" is discouraged (0 uses).
 New usage of "19.3vOLD" is discouraged (0 uses).
 New usage of "19.41rg" is discouraged (3 uses).
 New usage of "19.41rgVD" is discouraged (0 uses).
@@ -18222,8 +18223,10 @@ New usage of "sb4b" is discouraged (13 uses).
 New usage of "sb4bOLD" is discouraged (0 uses).
 New usage of "sb4e" is discouraged (1 uses).
 New usage of "sb4vOLD" is discouraged (0 uses).
+New usage of "sb56OLD" is discouraged (0 uses).
 New usage of "sb5ALT" is discouraged (0 uses).
 New usage of "sb5ALTVD" is discouraged (0 uses).
+New usage of "sb5OLD" is discouraged (0 uses).
 New usage of "sb5f" is discouraged (1 uses).
 New usage of "sb5rf" is discouraged (0 uses).
 New usage of "sb6f" is discouraged (2 uses).
@@ -18802,6 +18805,7 @@ Proof modification of "0nnnALT" is discouraged (11 steps).
 Proof modification of "0reALT" is discouraged (15 steps).
 Proof modification of "139prmALT" is discouraged (758 steps).
 Proof modification of "19.21a3con13vVD" is discouraged (107 steps).
+Proof modification of "19.36imvOLD" is discouraged (25 steps).
 Proof modification of "19.3vOLD" is discouraged (19 steps).
 Proof modification of "19.41rg" is discouraged (58 steps).
 Proof modification of "19.41rgVD" is discouraged (127 steps).
@@ -19157,7 +19161,6 @@ Proof modification of "bj-rexvw" is discouraged (34 steps).
 Proof modification of "bj-ru" is discouraged (22 steps).
 Proof modification of "bj-ru0" is discouraged (50 steps).
 Proof modification of "bj-ru1" is discouraged (27 steps).
-Proof modification of "bj-sb56" is discouraged (50 steps).
 Proof modification of "bj-sbceqgALT" is discouraged (143 steps).
 Proof modification of "bj-sbeqALT" is discouraged (44 steps).
 Proof modification of "bj-sbidmOLD" is discouraged (41 steps).
@@ -19175,7 +19178,8 @@ Proof modification of "bj-ssblem2" is discouraged (43 steps).
 Proof modification of "bj-sscon" is discouraged (48 steps).
 Proof modification of "bj-stabpeirce" is discouraged (22 steps).
 Proof modification of "bj-stdpc5" is discouraged (20 steps).
-Proof modification of "bj-subst" is discouraged (89 steps).
+Proof modification of "bj-subst" is discouraged (50 steps).
+Proof modification of "bj-substax12" is discouraged (89 steps).
 Proof modification of "bj-substw" is discouraged (49 steps).
 Proof modification of "bj-vecssmod" is discouraged (18 steps).
 Proof modification of "bj-vecssmodel" is discouraged (5 steps).
@@ -20188,8 +20192,10 @@ Proof modification of "sb3bOLD" is discouraged (24 steps).
 Proof modification of "sb4OLD" is discouraged (20 steps).
 Proof modification of "sb4bOLD" is discouraged (110 steps).
 Proof modification of "sb4vOLD" is discouraged (16 steps).
+Proof modification of "sb56OLD" is discouraged (25 steps).
 Proof modification of "sb5ALT" is discouraged (80 steps).
 Proof modification of "sb5ALTVD" is discouraged (110 steps).
+Proof modification of "sb5OLD" is discouraged (25 steps).
 Proof modification of "sbal1" is discouraged (149 steps).
 Proof modification of "sbal2OLD" is discouraged (157 steps).
 Proof modification of "sbc2or" is discouraged (134 steps).