Theorem exopxfr

Description: Transfer ordered-pair existence from/to single variable existence. (Contributed by NM, 26-Feb-2014) (Proof shortened by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Hypothesis	exopxfr.1	|- ( x = <. y , z >. -> ( ph <-> ps ) )
Assertion	exopxfr	|- ( E. x e. ( _V X. _V ) ph <-> E. y E. z ps )

Proof

Step	Hyp	Ref	Expression
1		exopxfr.1	|- ( x = <. y , z >. -> ( ph <-> ps ) )
2	1	rexxp	|- ( E. x e. ( _V X. _V ) ph <-> E. y e. _V E. z e. _V ps )
3		rexv	|- ( E. y e. _V E. z e. _V ps <-> E. y E. z e. _V ps )
4		rexv	|- ( E. z e. _V ps <-> E. z ps )
5	4	exbii	|- ( E. y E. z e. _V ps <-> E. y E. z ps )
6	2 3 5	3bitri	|- ( E. x e. ( _V X. _V ) ph <-> E. y E. z ps )