corrections

set.mm

@@ -28807,7 +28807,7 @@ generally appear in a single form (either definitional, but more often
     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 $.
-    $( $j usage 'rspw' avoids 'ax-8' 'df-clel' 'ax-10' 'ax-11' 'ax-12'; $)
+    $( $j usage 'rspw' avoids 'ax-10' 'ax-11' 'ax-12'; $)
   $}
 
   $( Restricted specialization.  (Contributed by NM, 17-Oct-1996.) $)
@@ -40066,7 +40066,7 @@ among classes ( ~ eq0 , as opposed to the weaker uniqueness among sets,
       FZGHUMICFZHZBJZDKZGUNUMCLUAUODUBZUNMZBNZDKZUQUOURUMMZUSNZDKVADUMUNUCVCUTD
       VCBUSNUTVBBUSVBACDTBADCOABCDEUDPQBUSUEPRPVAIBNZDKUQUTVDDUSIBUSICDTIIDCOIC
       DUFPQRVDUPDVDUPIBUPBUPUGSIJUPUHUIIBBBSBUJUKULRPPP $.
-    $( $j usage 'ab0' avoids 'df-clel' 'ax-8' 'ax-10' 'ax-11' 'ax-12'; $)
+    $( $j usage 'ab0w' avoids 'df-clel' 'ax-8' 'ax-10' 'ax-11' 'ax-12'; $)
   $}
 
   $( The class of sets verifying a property is the empty class if and only if