mopickALT

set.mm

@@ -553274,6 +553274,18 @@ relation with an intersection with the same Cartesian product (see also
       APZUFTABCUEDRUFUHUIACDSUAUB $.
   $}
 
+  ${
+    $d x y $.  $d y ph $.  $d y ps $.
+    $( "At most one" picks a variable value, eliminating an existential
+       quantifier.  Alternate proof of ~ mopick . (Contributed by Peter Mazsa,
+       18-Nov-2024.) $)
+    mopickALT $p |- ( ( E* x ph /\ E. x ( ph /\ ps ) ) -> ( ph -> ps ) ) $=
+      ( wmo wa wex wi wn weu wo moeu imor bitri bj-nexrt pm2.21 syl a1d
+    wal eupickbi sp syl6bi jaoi sylbi imp ) ACDZABECFZABGZUEACFZHZACI
+    ZJZUFUGGZUEUHUJGUKACKUHUJLMUIULUJUIUGUFUIAHUGACNABOPQUJUFUGCRUGAB
+    CSUGCTUAUBUCUD $.
+  $}
+
   $( Sufficient condition for transitivity of conjunctions inside existential
      quantifiers.  (Contributed by Peter Mazsa, 2-Oct-2018.) $)
   moantr $p |- ( E* x ps ->