Move two theorems out of Section 'Theorems requiring empty set existe…

…nce' when they do not require it. Add cross-links and clarify comments.

discouraged

@@ -19853,7 +19853,7 @@ Proof modification of "bj-19.21t0" is discouraged (39 steps).
 Proof modification of "bj-19.41al" is discouraged (51 steps).
 Proof modification of "bj-a1k" is discouraged (10 steps).
 Proof modification of "bj-ab0" is discouraged (39 steps).
-Proof modification of "bj-abex" is discouraged (35 steps).
+Proof modification of "bj-abex" is discouraged (32 steps).
 Proof modification of "bj-abf" is discouraged (13 steps).
 Proof modification of "bj-ablsscmn" is discouraged (10 steps).
 Proof modification of "bj-ablsscmnel" is discouraged (5 steps).

set.mm

@@ -34458,6 +34458,17 @@ general is seen either by substitution (when the variable ` V ` has no
       DLZMABNSTECDEOPFQR $.
   $}
 
+  ${
+    $d x A $.
+    $( Writing a set as a class abstraction.  This theorem looks artificial but
+       was added to characterize the class abstraction whose existence is
+       proved in ~ class2set .  (Contributed by NM, 13-Dec-2005.)  (Proof
+       shortened by Raph Levien, 30-Jun-2006.) $)
+    class2seteq $p |- ( A e. V -> { x e. A | A e. _V } = A ) $=
+      ( wcel cvv crab wceq elex wral cv ax-1 ralrimiv rabid2 sylibr eqcomd syl
+      ) BCDBEDZQABFZBGBCHQBRQQABIBRGQQABQAJBDKLQABMNOP $.
+  $}
+
   ${
     $d x A $.  $d x B $.  $d x ph $.
     nelrdva.1 $e |- ( ( ph /\ x e. A ) -> x =/= B ) $.
@@ -50309,6 +50320,22 @@ holding in an empty domain (see Axiom A5 and Rule R2 of [LeBlanc]
       ( cpw wcel wss wb elpw2g ax-mp mpbir ) ABFGZABHZEBCGMNIDABCJKL $.
   $}
 
+  ${
+    $d A x y $.  $d A y z $.
+    $( Two equivalent ways to express the Power Set Axiom.  Note that ~ ax-pow
+       is not used by the proof.  When ~ ax-pow is assumed and ` A ` is a set,
+       both sides of the biconditional hold.  In ZF, both sides hold if and
+       only if ` A ` is a set (see ~ pwexr ).  (Contributed by NM,
+       22-Jun-2009.) $)
+    axpweq $p |- ( ~P A e. _V
+                     <-> E. x A. y ( A. z ( z e. y -> z e. A ) -> y e. x ) ) $=
+      ( cpw cvv wcel cv wex wel wal pwidg wceq pweq eleq2d spcegv mpd wss bitri
+      wi elex exlimiv impbii vex elpw2 pwss dfss2 imbi1i albii exbii ) DEZFGZUK
+      AHZEZGZAIZCBJCHDGTCKZBAJZTZBKZAIULUPULUKUKEZGZUPUKFLUOVBAUKFUMUKMUNVAUKUM
+      UKNOPQUOULAUKUNUAUBUCUOUTAUOUKUMRZUTUKUMAUDUEVCBHZDRZURTZBKUTBDUMUFVFUSBV
+      EUQURCVDDUGUHUISSUJS $.
+  $}
+
   ${
     $d A x $.
     $( The power set of a set is never a subset.  (Contributed by Stefan
@@ -50347,26 +50374,21 @@ holding in an empty domain (see Axiom A5 and Rule R2 of [LeBlanc]
 
   ${
     $d x A $.
-    $( Construct, from any class ` A ` , a set equal to it when the class
-       exists and equal to the empty set when the class is proper.  This
-       theorem shows that the constructed set always exists.  (Contributed by
-       NM, 16-Oct-2003.) $)
+    $( The class of elements of ` A ` "such that ` A ` is a set" is a set.
+       That class is equal to ` A ` when ` A ` is a set (see ~ class2seteq )
+       and to the empty set when ` A ` is a proper class.  (Contributed by NM,
+       16-Oct-2003.) $)
     class2set $p |- { x e. A | A e. _V } e. _V $=
       ( wcel crab rabexg wn c0 wrex wceq cv simpl nrexdv rabn0 necon1bbii sylib
       cvv 0ex eqeltrdi pm2.61i ) BPCZTABDZPCTABPETFZUAGPUBTABHZFUAGIUBTABUBAJBC
       KLUCUAGTABMNOQRS $.
-
-    $( Equality theorem based on ~ class2set .  (Contributed by NM,
-       13-Dec-2005.)  (Proof shortened by Raph Levien, 30-Jun-2006.) $)
-    class2seteq $p |- ( A e. V -> { x e. A | A e. _V } = A ) $=
-      ( wcel cvv crab wceq elex wral cv ax-1 ralrimiv rabid2 sylibr eqcomd syl
-      ) BCDBEDZQABFZBGBCHQBRQQABIBRGQQABQAJBDKLQABMNOP $.
   $}
 
   $( Every power class contains the empty set.  (Contributed by NM,
      25-Oct-2007.) $)
   0elpw $p |- (/) e. ~P A $=
     ( c0 cpw wcel wss 0ss 0ex elpw mpbir ) BACDBAEAFBAGHI $.
+
   $( A power class is never empty.  (Contributed by NM, 3-Sep-2018.) $)
   pwne0 $p |- ~P A =/= (/) $=
     ( c0 cpw 0elpw ne0ii ) BACADE $.
@@ -50426,22 +50448,6 @@ holding in an empty domain (see Axiom A5 and Rule R2 of [LeBlanc]
   intv $p |- |^| _V = (/) $=
     ( c0 cvv wcel cint wceq 0ex int0el ax-mp ) ABCBDAEFBGH $.
 
-  ${
-    $d A x y $.  $d A y z $.
-    $( Two equivalent ways to express the Power Set Axiom.  Note that ~ ax-pow
-       is not used by the proof.  When ~ ax-pow is assumed and ` A ` is a set,
-       both sides of the biconditional hold.  In ZF, both sides hold if and
-       only if ` A ` is a set (see ~ pwexr ).  (Contributed by NM,
-       22-Jun-2009.) $)
-    axpweq $p |- ( ~P A e. _V
-                     <-> E. x A. y ( A. z ( z e. y -> z e. A ) -> y e. x ) ) $=
-      ( cpw cvv wcel cv wex wel wal pwidg wceq pweq eleq2d spcegv mpd wss bitri
-      wi elex exlimiv impbii vex elpw2 pwss dfss2 imbi1i albii exbii ) DEZFGZUK
-      AHZEZGZAIZCBJCHDGTCKZBAJZTZBKZAIULUPULUKUKEZGZUPUKFLUOVBAUKFUMUKMUNVAUKUM
-      UKNOPQUOULAUKUNUAUBUCUOUTAUOUKUMRZUTUKUMAUDUEVCBHZDRZURTZBKUTBDUMUFVFUSBV
-      EUQURCVDDUGUHUISSUJS $.
-  $}
-
 
 $(
 #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
@@ -557757,7 +557763,7 @@ equivalent to the existence of binary unions and of nullary unions (the
   ${
     $d x y z t $.  $d A y $.
     $( Existence of the result of the adjunction (generalized only in the first
-       term is this suffices for current applications).  (Contributed by BJ,
+       term since this suffices for current applications).  (Contributed by BJ,
        19-Jan-2025.)  (Proof modification is discouraged.) $)
     bj-adjg1 $p |- ( A e. V -> ( A u. { x } ) e. _V ) $=
       ( vy vt vz cv csn cun cvv wcel wceq uneq1 eleq1d wel weq wo wb wal spi