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

Metamath Proof Explorer

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