Metamath Proof Explorer

Theorem euop2

Description: Transfer existential uniqueness to second member of an ordered pair. (Contributed by NM, 10-Apr-2004)

Ref Expression
Hypothesis euop2.1 
|- A e. _V
Assertion euop2 
|- ( E! x E. y ( x = <. A , y >. /\ ph ) <-> E! y ph )

Proof

Step Hyp Ref Expression
1 euop2.1 
 |-  A e. _V
2 opex 
 |-  <. A , y >. e. _V
3 1 moop2 
 |-  E* y x = <. A , y >.
4 2 3 euxfr2w 
 |-  ( E! x E. y ( x = <. A , y >. /\ ph ) <-> E! y ph )