Shorten nfuni. Mathbox: bj-elsn0.

set.mm

@@ -43748,16 +43748,6 @@ there is another (different) element of the class ` V ` which is an
       P $.
   $}
 
-  ${
-    $d y z A $.  $d x y z $.
-    nfuni.1 $e |- F/_ x A $.
-    $( Bound-variable hypothesis builder for union.  (Contributed by NM,
-       30-Dec-1996.)  (Proof shortened by Andrew Salmon, 27-Aug-2011.) $)
-    nfuni $p |- F/_ x U. A $=
-      ( vy vz cuni wel wrex cab dfuni2 nfv nfrex nfab nfcxfr ) ABFDEGZEBHZDIDEB
-      JPADOAEBCOAKLMN $.
-  $}
-
   ${
     $d y z A $.  $d x y z $.  $d y z ph $.
     nfunid.3 $e |- ( ph -> F/_ x A ) $.
@@ -43767,6 +43757,14 @@ there is another (different) element of the class ` V ` which is an
       FCIZEJEFCKARBEAELAQBFCAFLDAQBMNOP $.
   $}
 
+  ${
+    nfuni.1 $e |- F/_ x A $.
+    $( Bound-variable hypothesis builder for union.  (Contributed by NM,
+       30-Dec-1996.)  (Proof shortened by Andrew Salmon, 27-Aug-2011.) $)
+    nfuni $p |- F/_ x U. A $=
+      ( wnfc cuni id nfunid ax-mp ) ABDZABEDCIABIFGH $.
+  $}
+
   ${
     $d x y A $.  $d x y B $.
     $( Equality theorem for class union.  Exercise 15 of [TakeutiZaring] p. 18.
@@ -535798,7 +535796,8 @@ sethood hypotheses (compare ~ opth ).  (Contributed by BJ, 6-Oct-2018.) $)
   $( Two classes are related by the membership relation if and only if they are
      related by the membership relation (i.e., the first is an element of the
      second) and the second is a set (hence so is the first).  TODO: move to
-     Main after reordering to have ~ brrelex2i available.  (Contributed by BJ,
+     Main after reordering to have ~ brrelex2i available.  Check if it is
+     shorter to prove ~ bj-epelg first or ~ bj-epelb first. (Contributed by BJ,
      14-Jul-2023.) $)
   bj-epelb $p |- ( A _E B <-> ( A e. B /\ B e. _V ) ) $=
     ( cep wbr cvv wcel wa rele brrelex2i pm4.71i epelg pm5.32ri bitri ) ABCDZNB
@@ -536935,6 +536934,15 @@ both are sets (all three classes are equal, so they all belong to ` V ` ,
     wceq sseqin2 jca ) ABDZCEZABQZFZAGEBGEUCACUBUATAQZACEZUBABHUDABIABJKUDUAUET
     ACLMNOUCBCUBUATBQZBCEZUBBAHUFBAPBARKUFUAUGTBCLMNOS $.
 
+  $( If the intersection of two classes is a set, then these classes are equal
+     if and only if one is an element of the singleton formed on the other.
+     Stronger form of ~ elsng and ~ elsn2g (which could be proved from it).
+     (Contributed by BJ, 20-Jan-2024.). $)
+  bj-elsn0 $p |- ( ( A i^i B ) e. V -> ( A e. { B } <-> A = B ) ) $=
+    ( cin wcel csn wceq elsni wi wa cvv bj-inexeqex simpl elsng biimprd 3syl ex
+    pm2.43d impbid2 ) ABDCEZABFEZABGZABHTUBUATUBUBUAIZTUBJAKEZBKEZJUDUCABCLUDUE
+    MUDUAUBABKNOPQRS $.
+
   $( Characterization of the ordered pair elements of the identity relation
      when the intersection of their components are sets.  Note that the
      antecedent is more general than either component being a set.