Metamath Proof Explorer


Theorem mosubop

Description: "At most one" remains true inside ordered pair quantification. (Contributed by NM, 28-May-1995)

Ref Expression
Hypothesis mosubop.1
|- E* x ph
Assertion mosubop
|- E* x E. y E. z ( A = <. y , z >. /\ ph )

Proof

Step Hyp Ref Expression
1 mosubop.1
 |-  E* x ph
2 1 gen2
 |-  A. y A. z E* x ph
3 mosubopt
 |-  ( A. y A. z E* x ph -> E* x E. y E. z ( A = <. y , z >. /\ ph ) )
4 2 3 ax-mp
 |-  E* x E. y E. z ( A = <. y , z >. /\ ph )