This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem exopxfr2

Description: Transfer ordered-pair existence from/to single variable existence. (Contributed by NM, 26-Feb-2014)

Ref Expression
Hypothesis exopxfr2.1 
|- ( x = <. y , z >. -> ( ph <-> ps ) )
Assertion exopxfr2 
|- ( Rel A -> ( E. x e. A ph <-> E. y E. z ( <. y , z >. e. A /\ ps ) ) )

Proof

Step Hyp Ref Expression
1 exopxfr2.1 
 |-  ( x = <. y , z >. -> ( ph <-> ps ) )
2 df-rel 
 |-  ( Rel A <-> A C_ ( _V X. _V ) )
3 2 biimpi 
 |-  ( Rel A -> A C_ ( _V X. _V ) )
4 3 sseld 
 |-  ( Rel A -> ( x e. A -> x e. ( _V X. _V ) ) )
5 4 adantrd 
 |-  ( Rel A -> ( ( x e. A /\ ph ) -> x e. ( _V X. _V ) ) )
6 5 pm4.71rd 
 |-  ( Rel A -> ( ( x e. A /\ ph ) <-> ( x e. ( _V X. _V ) /\ ( x e. A /\ ph ) ) ) )
7 6 rexbidv2 
 |-  ( Rel A -> ( E. x e. A ph <-> E. x e. ( _V X. _V ) ( x e. A /\ ph ) ) )
8 eleq1 
 |-  ( x = <. y , z >. -> ( x e. A <-> <. y , z >. e. A ) )
9 8 1 anbi12d 
 |-  ( x = <. y , z >. -> ( ( x e. A /\ ph ) <-> ( <. y , z >. e. A /\ ps ) ) )
10 9 exopxfr 
 |-  ( E. x e. ( _V X. _V ) ( x e. A /\ ph ) <-> E. y E. z ( <. y , z >. e. A /\ ps ) )
11 7 10 bitrdi 
 |-  ( Rel A -> ( E. x e. A ph <-> E. y E. z ( <. y , z >. e. A /\ ps ) ) )