moeu2 mopickr

set.mm

@@ -581971,6 +581971,23 @@ relation with an intersection with the same Cartesian product (see also
       APZUFTABCUEDRUFUHUIACDSUAUB $.
   $}
 
+  $( Uniqueness is equivalent to non-existence or unique existence.  Alternate
+     definition of the at-most-one quantifier, in terms of the existential
+     quantifier and the unique existential quantifier.  (Contributed by Peter
+     Mazsa, 19-Nov-2024.) $)
+  moeu2 $p |- ( E* x ph <-> ( -. E. x ph \/ E! x ph ) ) $=
+    ( wmo wex weu wi wn wo moeu imor bitri ) ABCABDZABEZFLGMHABILMJK $.
+
+  $( "At most one" picks a variable value, eliminating an existential
+     quantifier.  The proof begins with references *2.21 ( ~ pm2.21 ) and
+     *14.26 ( ~ eupickbi ) from [WhiteheadRussell] p. 104 and p. 183.
+     (Contributed by Peter Mazsa, 18-Nov-2024.)
+     (Proof modification is discouraged.) $)
+  mopickr $p |- ( ( E* x ps /\ E. x ( ph /\ ps ) ) -> ( ps -> ph ) ) $=
+    ( wmo wa wex wi exancom wn weu wo moeu2 bj-nexrt pm2.21 syl a1d eupickbi sp
+    wal syl6bi jaoi sylbi syl5bi imp ) BCDZABECFZBAGZUFBAECFZUEUGABCHUEBCFIZBCJ
+    ZKUHUGGZBCLUIUKUJUIUGUHUIBIUGBCMBANOPUJUHUGCSUGBACQUGCRTUAUBUCUD $.
+
   $( Sufficient condition for transitivity of conjunctions inside existential
      quantifiers.  (Contributed by Peter Mazsa, 2-Oct-2018.) $)
   moantr $p |- ( E* x ps ->