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

Metamath Proof Explorer

Theorem copsex2g

Description: Implicit substitution inference for ordered pairs. (Contributed by NM, 28-May-1995) Use a similar proof to copsex4g to reduce axiom usage. (Revised by SN, 1-Sep-2024)

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

Proof

Step Hyp Ref Expression
1 copsex2g.1 
 |-  ( ( x = A /\ y = B ) -> ( ph <-> ps ) )
2 eqcom 
 |-  ( <. A , B >. = <. x , y >. <-> <. x , y >. = <. A , B >. )
3 vex 
 |-  x e. _V
4 vex 
 |-  y e. _V
5 3 4 opth 
 |-  ( <. x , y >. = <. A , B >. <-> ( x = A /\ y = B ) )
6 2 5 bitri 
 |-  ( <. A , B >. = <. x , y >. <-> ( x = A /\ y = B ) )
7 6 anbi1i 
 |-  ( ( <. A , B >. = <. x , y >. /\ ph ) <-> ( ( x = A /\ y = B ) /\ ph ) )
8 7 2exbii 
 |-  ( E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) <-> E. x E. y ( ( x = A /\ y = B ) /\ ph ) )
9 id 
 |-  ( ( x = A /\ y = B ) -> ( x = A /\ y = B ) )
10 9 1 cgsex2g 
 |-  ( ( A e. V /\ B e. W ) -> ( E. x E. y ( ( x = A /\ y = B ) /\ ph ) <-> ps ) )
11 8 10 bitrid 
 |-  ( ( A e. V /\ B e. W ) -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) <-> ps ) )