tweaks

set.mm

@@ -28792,8 +28792,8 @@ generally appear in a single form (either definitional, but more often
   ${
     $d x y A $.  $d x ps $.  $d y ph $.
     rspw.1 $e |- ( x = y -> ( ph <-> ps ) ) $.
-    $( Restricted specialization.  Weak version ~ rsp , requiring fewer axioms.
-       (Contributed by Gino Giotto, 3-Oct-2024.) $)
+    $( Restricted specialization.  Weak version of ~ rsp , requiring ~ ax-8 ,
+       but not ~ ax-12 .  (Contributed by Gino Giotto, 3-Oct-2024.) $)
     rspw $p |- ( A. x e. A ph -> ( x e. A -> ph ) ) $=
       ( wral cv wcel wi wal df-ral weq eleq1w imbi12d spw sylbi ) ACEGCHEIZAJZC
       KSACELSDHEIZBJCDCDMRTABCDENFOPQ $.
@@ -74440,7 +74440,7 @@ also define a subset of the complex numbers ( ~ df-nn ) with analogous
        more traditional statement of mathematical induction as a theorem
        schema, with a basis and an induction step, is derived from this theorem
        as Theorem ~ findes .  (Contributed by NM, 18-Feb-2004.)  Avoid
-       ~ ax-12 .  (Revised by Gino Giotto, 3-Oct-2024.) $)
+       ~ ax-10 , ~ ax-12 .  (Revised by Gino Giotto, 3-Oct-2024.) $)
     peano5 $p |- ( ( (/) e. A /\
                  A. x e. _om ( x e. A -> suc x e. A ) ) -> _om C_ A ) $=
       ( vz vy c0 wcel cv csuc wi com wral wa cdif wceq wss wrex wne eleq1 exp32
@@ -74457,7 +74457,7 @@ also define a subset of the complex numbers ( ~ df-nn ) with analogous
       JXLXRYDYCIXJXLXIJFXRXBXIJRXHVBVDXRYDXCXSYDXCLXRXHWTFTXSXHXBWTVEXHJBVFVGSV
       HVIVNVOXTXJXGXIBXBVJVKVLVMVPVQSVRVSWFVTWAXDWTEJWBWTJOWTEQXDWCJBWDCJWTWGWE
       WHWIJBWJWK $.
-    $( $j usage 'peano5' avoids 'ax-12' 'ax-inf' 'ax-inf2' 'ax-reg'; $)
+    $( $j usage 'peano5' avoids 'ax-10' 'ax-12' 'ax-inf' 'ax-inf2' 'ax-reg'; $)
   $}
 
   ${