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 ) ) )