Theorem copsex2gb

Description: Implicit substitution inference for ordered pairs. Compare copsex2ga . (Contributed by NM, 12-Mar-2014)

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

Proof

Step	Hyp	Ref	Expression
1		copsex2ga.1	|- ( A = <. x , y >. -> ( ph <-> ps ) )
2		elvv	|- ( A e. ( _V X. _V ) <-> E. x E. y A = <. x , y >. )
3	2	anbi1i	|- ( ( A e. ( _V X. _V ) /\ ph ) <-> ( E. x E. y A = <. x , y >. /\ ph ) )
4		19.41vv	|- ( E. x E. y ( A = <. x , y >. /\ ph ) <-> ( E. x E. y A = <. x , y >. /\ ph ) )
5	1	pm5.32i	|- ( ( A = <. x , y >. /\ ph ) <-> ( A = <. x , y >. /\ ps ) )
6	5	2exbii	|- ( E. x E. y ( A = <. x , y >. /\ ph ) <-> E. x E. y ( A = <. x , y >. /\ ps ) )
7	3 4 6	3bitr2ri	|- ( E. x E. y ( A = <. x , y >. /\ ps ) <-> ( A e. ( _V X. _V ) /\ ph ) )