Theorem copsex2ga

Description: Implicit substitution inference for ordered pairs. Compare copsex2g . (Contributed by NM, 26-Feb-2014) (Proof shortened by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Hypothesis	copsex2ga.1	|- ( A = <. x , y >. -> ( ph <-> ps ) )
Assertion	copsex2ga	|- ( A e. ( V X. W ) -> ( ph <-> E. x E. y ( A = <. x , y >. /\ ps ) ) )

Proof

Step	Hyp	Ref	Expression
1		copsex2ga.1	|- ( A = <. x , y >. -> ( ph <-> ps ) )
2		xpss	|- ( V X. W ) C_ ( _V X. _V )
3	2	sseli	|- ( A e. ( V X. W ) -> A e. ( _V X. _V ) )
4	1	copsex2gb	|- ( E. x E. y ( A = <. x , y >. /\ ps ) <-> ( A e. ( _V X. _V ) /\ ph ) )
5	4	baibr	|- ( A e. ( _V X. _V ) -> ( ph <-> E. x E. y ( A = <. x , y >. /\ ps ) ) )
6	3 5	syl	|- ( A e. ( V X. W ) -> ( ph <-> E. x E. y ( A = <. x , y >. /\ ps ) ) )