[move] reuxfr1dd; [fix] upciclem1 description

Author: zwang123

set.mm

@@ -833039,6 +833039,29 @@ additional condition (deduction form).  See ~ ralbidc for a more
     wreu reu5 ) ACBDZAEZSAFZGHABIZHABJZGSAKHABQTUBUAUCABLABMNSAOHABRP $.
 
 
+$(
+-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
+  The universal class
+-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
+$)
+
+  ${
+    $d x y ph $.  $d y ps $.  $d x ch $.  $d x A $.  $d x y B $.  $d x y C $.
+    reuxfr1dd.1 $e |- ( ( ph /\ y e. C ) -> A e. B ) $.
+    reuxfr1dd.2 $e |- ( ( ph /\ x e. B ) -> E! y e. C x = A ) $.
+    reuxfr1dd.3 $e |- ( ( ph /\ ( y e. C /\ x = A ) ) -> ( ps <-> ch ) ) $.
+    $( Transfer existential uniqueness from a variable ` x ` to another
+       variable ` y ` contained in expression ` A ` .  Simplifies ~ reuxfr1d .
+       (Contributed by Zhi Wang, 20-Sep-2025.) $)
+    reuxfr1dd $p |- ( ph -> ( E! x e. B ps <-> E! y e. C ch ) ) $=
+      ( wreu cv wceq wa wrex wcel syl anass bitrd biantrurd wb r19.41v pm5.32da
+      reurex 3bitr3g rexbidv2 bitr3id adantr reubidva wrmo reurmo reuxfrd ) ABD
+      GLDMZFNZCOZEHPZDGLCEHLABUQDGAUNGQZOZBUOEHPZBOZUQUSUTBUSUOEHLZUTJUOEHUERUA
+      AVAUQUBURVAUOBOZEHPAUQUOBEHUCAVCUPEHHAEMHQZUOOZBOVECOVDVCOVDUPOAVEBCKUDVD
+      UOBSVDUOCSUFUGUHUITUJACDEFGHIUSVBUOEHUKJUOEHULRUMT $.
+  $}
+
+
 $(
 -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
   The empty set
@@ -835527,7 +835550,8 @@ have GLB (expanded version).  (Contributed by Zhi Wang,
            n = ( ( ( X G y ) ` k ) ( <. Z , ( F ` X ) >. O ( F ` y ) ) M ) ) $.
     upciclem1.y $e |- ( ph -> Y e. B ) $.
     upciclem1.n $e |- ( ph -> N e. ( Z J ( F ` Y ) ) ) $.
-    $( Lemma for ~ upcic .  (Contributed by Zhi Wang, 16-Sep-2025.) $)
+    $( Lemma for ~ upcic , ~ upeu , and ~ upeu2 .  (Contributed by Zhi Wang,
+       16-Sep-2025.) $)
     upciclem1 $p |- ( ph -> E! l e. ( X H Y )
                             N = ( ( ( X G Y ) ` l )
                             ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) $=
@@ -835542,22 +835566,6 @@ have GLB (expanded version).  (Contributed by Zhi Wang,
       OVFUJUTUPVAVBVC $.
   $}
 
-  ${
-    $d x y ph $.  $d y ps $.  $d x ch $.  $d x A $.  $d x y B $.  $d x y C $.
-    reuxfr1dd.1 $e |- ( ( ph /\ y e. C ) -> A e. B ) $.
-    reuxfr1dd.2 $e |- ( ( ph /\ x e. B ) -> E! y e. C x = A ) $.
-    reuxfr1dd.3 $e |- ( ( ph /\ ( y e. C /\ x = A ) ) -> ( ps <-> ch ) ) $.
-    $( Transfer existential uniqueness from a variable ` x ` to another
-       variable ` y ` contained in expression ` A ` .  Simplifies ~ reuxfr1d .
-       (Contributed by Zhi Wang, 20-Sep-2025.) $)
-    reuxfr1dd $p |- ( ph -> ( E! x e. B ps <-> E! y e. C ch ) ) $=
-      ( wreu cv wceq wa wrex wcel syl anass bitrd biantrurd wb r19.41v pm5.32da
-      reurex 3bitr3g rexbidv2 bitr3id adantr reubidva wrmo reurmo reuxfrd ) ABD
-      GLDMZFNZCOZEHPZDGLCEHLABUQDGAUNGQZOZBUOEHPZBOZUQUSUTBUSUOEHLZUTJUOEHUERUA
-      AVAUQUBURVAUOBOZEHPAUQUOBEHUCAVCUPEHHAEMHQZUOOZBOVECOVDVCOVDUPOAVEBCKUDVD
-      UOBSVDUOCSUFUGUHUITUJACDEFGHIUSVBUOEHUKJUOEHULRUMT $.
-  $}
-
   ${
     $d .x. k $.  $d C k $.  $d F k $.  $d G k $.  $d H k $.  $d X k $.
     $d Y k $.  $d Z k $.  $d k ph $.