move section russel's paradox to main (#3253)

cbvabvw is equivalent to cbvabv now (see #3165)
so likewise, change cbvrabv to match cbvrabvw and remove cbvrabvw

move rru to main
now that cbvrabvw --> cbvrabv, the only change is avoiding df-nel,
which happened 3 days later
use rru in pwnss which is basically like minimize so no tag added

Author: icecream17

changes-set.txt

@@ -27,6 +27,7 @@ make a github issue.)
 
 DONE:
 Date      Old       New         Notes
+14-Jun-23 rru       [same]      moved from SN's mathbox to main set.mm
 10-Jun-23 sbtv      [same]      moved fron SN's mathbox to main set.mm
  8-Jun-23 rnmptc    [same]      moved from GS's mathbox to main set.mm
  8-Jun-23 eqneltri  [same]      moved from GS's mathbox to main set.mm

discouraged

@@ -14213,6 +14213,7 @@ New usage of "cbvabvOLD" is discouraged (0 uses).
 New usage of "cbveuALT" is discouraged (0 uses).
 New usage of "cbvexsv" is discouraged (2 uses).
 New usage of "cbvmoOLD" is discouraged (0 uses).
+New usage of "cbvrabvOLD" is discouraged (0 uses).
 New usage of "ccat2s1fvwALT" is discouraged (0 uses).
 New usage of "ccatopthOLD" is discouraged (0 uses).
 New usage of "ccats1swrdeqOLD" is discouraged (2 uses).
@@ -18592,6 +18593,7 @@ Proof modification of "cbvabvOLD" is discouraged (12 steps).
 Proof modification of "cbveuALT" is discouraged (48 steps).
 Proof modification of "cbvexsv" is discouraged (29 steps).
 Proof modification of "cbvmoOLD" is discouraged (48 steps).
+Proof modification of "cbvrabvOLD" is discouraged (19 steps).
 Proof modification of "ccat2s1fvwALT" is discouraged (149 steps).
 Proof modification of "ccatopthOLD" is discouraged (245 steps).
 Proof modification of "ccats1swrdeqOLD" is discouraged (203 steps).

set.mm

@@ -29995,11 +29995,25 @@ choice between (what we call) a "definitional form" where the shorter
   $}
 
   ${
-    $d x A $.  $d y A $.  $d y ph $.  $d x ps $.
+    $d x y A $.  $d y ph $.  $d x ps $.
     cbvrabv.1 $e |- ( x = y -> ( ph <-> ps ) ) $.
     $( Rule to change the bound variable in a restricted class abstraction,
-       using implicit substitution.  (Contributed by NM, 26-May-1999.) $)
+       using implicit substitution.  (Contributed by NM, 26-May-1999.)  Require
+       ` x ` , ` y ` be disjoint to avoid ~ ax-11 and ~ ax-13 .  (Revised by
+       Steven Nguyen, 4-Dec-2022.) $)
     cbvrabv $p |- { x e. A | ph } = { y e. A | ps } $=
+      ( cv wcel wa cab crab weq eleq1w anbi12d cbvabv df-rab 3eqtr4i ) CGEHZAIZ
+      CJDGEHZBIZDJACEKBDEKSUACDCDLRTABCDEMFNOACEPBDEPQ $.
+  $}
+
+  ${
+    $d x A $.  $d y A $.  $d y ph $.  $d x ps $.
+    cbvrabvOLD.1 $e |- ( x = y -> ( ph <-> ps ) ) $.
+    $( Obsolete version of ~ cbvrabv as of 14-Jun-2023.  Rule to change the
+       bound variable in a restricted class abstraction, using implicit
+       substitution.  (Contributed by NM, 26-May-1999.)
+       (New usage is discouraged.)  (Proof modification is discouraged.) $)
+    cbvrabvOLD $p |- { x e. A | ph } = { y e. A | ps } $=
       ( nfcv nfv cbvrab ) ABCDECEGDEGADHBCHFI $.
   $}
 
@@ -32893,6 +32907,20 @@ something like (wi (wceq (cv vx) (cv vy)) wph) ) into just (wcdeq vx vy
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
 $)
 
+  ${
+    $d x y A $.
+    $( Relative version of Russell's paradox ~ ru (which corresponds to the
+       case ` A = _V ` ).
+
+       Originally a subproof in ~ pwnss .  (Contributed by Stefan O'Rear,
+       22-Feb-2015.)  Avoid ~ df-nel .  (Revised by Steven Nguyen,
+       23-Nov-2022.) $)
+    rru $p |- -. { x e. A | -. x e. x } e. A $=
+      ( vy wel wn crab wcel wa wb cv eleq12 anidms notbid cbvrabv elrab2 pclem6
+      wceq weq ax-mp ) AADZEZABFZUBGZUBBGZUCEZHIUDECCDZEZUECUBBUBCJZUBQZUFUCUIU
+      FUCIUHUBUHUBKLMUAUGACBACRZTUFUJTUFIAJZUHUKUHKLMNOUCUDPS $.
+  $}
+
   ${
     $d x y $.
     $( Russell's Paradox.  Proposition 4.14 of [TakeutiZaring] p. 14.
@@ -45891,15 +45919,12 @@ holding in an empty domain (see Axiom A5 and Rule R2 of [LeBlanc]
   $}
 
   ${
-    $d A x y $.  $d V x y $.
+    $d A x $.
     $( The power set of a set is never a subset.  (Contributed by Stefan
        O'Rear, 22-Feb-2015.) $)
     pwnss $p |- ( A e. V -> -. ~P A C_ A ) $=
-      ( vx vy cpw cv wnel crab wcel wn wa wb eleq12 anidms notbid df-nel syl5bb
-      wss wceq cbvrabv elrab2 pclem6 ax-mp ssel mtoi ssrab2 elpw2g mpbiri nsyl3
-      ) AEZARZCFZULGZCAHZUJIZABIZUKUOUNAIZUNUNIZUQURJZKLUQJDFZUTIZJZUSDUNAUNUTU
-      NSZVAURVCVAURLUTUNUTUNMNOUMVBCDAUMULULIZJULUTSZVBULULPVEVDVAVEVDVALULUTUL
-      UTMNOQTUAURUQUBUCUJAUNUDUEUPUOUNARUMCAUFUNABUGUHUI $.
+      ( vx cpw wss wel wn crab wcel rru ssel mtoi ssrab2 elpw2g mpbiri nsyl3 )
+      ADZAEZCCFGZCAHZQIZABIZRUATAICAJQATKLUBUATAESCAMTABNOP $.
   $}
 
   $( No set equals its power set.  The sethood antecedent is necessary; compare
@@ -616091,47 +616116,6 @@ fixed reference functional determined by this vector (corresponding to
   $}
 
 
-$(
-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
-  Russell's paradox
-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
-$)
-
-  ${
-    $d x y $.  $d y z ph $.  $d x z ps $.
-    cbvabvw.1 $e |- ( x = y -> ( ph <-> ps ) ) $.
-    $( Version of ~ cbvabv with a distinct variable condition on x and y, which
-       removes dependencies on ~ ax-11 and ~ ax-13 .  (Contributed by Steven
-       Nguyen, 4-Dec-2022.) $)
-    cbvabvw $p |- { x | ph } = { y | ps } $=
-      ( vz cab wsb cv wcel weq wi wal equequ1 imbi12d cbvalvw sb6 3bitr4i eqriv
-      df-clab ) FACGZBDGZACFHZBDFHZFIZUAJUEUBJCFKZALZCMDFKZBLZDMUCUDUGUICDCDKUF
-      UHABCDFNEOPACFQBDFQRAFCTBFDTRS $.
-
-    $d x y A $.
-    $( Version of ~ cbvrabv with a distinct variable condition on x and y,
-       which removes dependencies on ~ ax-11 and ~ ax-13 .  (Contributed by
-       Steven Nguyen, 4-Dec-2022.) $)
-    cbvrabvw $p |- { x e. A | ph } = { y e. A | ps } $=
-      ( cv wcel wa cab crab weq eleq1w anbi12d cbvabvw df-rab 3eqtr4i ) CGEHZAI
-      ZCJDGEHZBIZDJACEKBDEKSUACDCDLRTABCDEMFNOACEPBDEPQ $.
-  $}
-
-  ${
-    $d x y A $.
-    $( Relative version of Russell's paradox ~ ru (which corresponds to the
-       case ` A = _V ` ).
-
-       Originally a subproof in ~ pwnss .  (Contributed by Stefan O'Rear,
-       22-Feb-2015.)  Remove usage of ~ ax-13 .  (Revised by Steven Nguyen,
-       20-Nov-2022.) $)
-    rru $p |- -. { x e. A | -. x e. x } e. A $=
-      ( vy wel wn crab wcel wa wb wceq eleq12 anidms notbid weq cbvrabvw elrab2
-      cv pclem6 ax-mp ) AADZEZABFZUBGZUBBGZUCEZHIUDECCDZEZUECUBBUBCQZUBJZUFUCUI
-      UFUCIUHUBUHUBKLMUAUGACBACNZTUFUJTUFIAQZUHUKUHKLMOPUCUDRS $.
-  $}
-
-
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
   Arithmetic theorems