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

Metamath Proof Explorer

Theorem copsex4g

Description: An implicit substitution inference for 2 ordered pairs. (Contributed by NM, 5-Aug-1995)

Ref Expression
Hypothesis copsex4g.1 
|- ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) -> ( ph <-> ps ) )
Assertion copsex4g 
|- ( ( ( A e. R /\ B e. S ) /\ ( C e. R /\ D e. S ) ) -> ( E. x E. y E. z E. w ( ( <. A , B >. = <. x , y >. /\ <. C , D >. = <. z , w >. ) /\ ph ) <-> ps ) )

Proof

Step Hyp Ref Expression
1 copsex4g.1 
 |-  ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) -> ( 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 eqcom 
 |-  ( <. C , D >. = <. z , w >. <-> <. z , w >. = <. C , D >. )
8 vex 
 |-  z e. _V
9 vex 
 |-  w e. _V
10 8 9 opth 
 |-  ( <. z , w >. = <. C , D >. <-> ( z = C /\ w = D ) )
11 7 10 bitri 
 |-  ( <. C , D >. = <. z , w >. <-> ( z = C /\ w = D ) )
12 6 11 anbi12i 
 |-  ( ( <. A , B >. = <. x , y >. /\ <. C , D >. = <. z , w >. ) <-> ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) )
13 12 anbi1i 
 |-  ( ( ( <. A , B >. = <. x , y >. /\ <. C , D >. = <. z , w >. ) /\ ph ) <-> ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) /\ ph ) )
14 13 a1i 
 |-  ( ( ( A e. R /\ B e. S ) /\ ( C e. R /\ D e. S ) ) -> ( ( ( <. A , B >. = <. x , y >. /\ <. C , D >. = <. z , w >. ) /\ ph ) <-> ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) /\ ph ) ) )
15 14 4exbidv 
 |-  ( ( ( A e. R /\ B e. S ) /\ ( C e. R /\ D e. S ) ) -> ( E. x E. y E. z E. w ( ( <. A , B >. = <. x , y >. /\ <. C , D >. = <. z , w >. ) /\ ph ) <-> E. x E. y E. z E. w ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) /\ ph ) ) )
16 id 
 |-  ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) -> ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) )
17 16 1 cgsex4g 
 |-  ( ( ( A e. R /\ B e. S ) /\ ( C e. R /\ D e. S ) ) -> ( E. x E. y E. z E. w ( ( ( x = A /\ y = B ) /\ ( z = C /\ w = D ) ) /\ ph ) <-> ps ) )
18 15 17 bitrd 
 |-  ( ( ( A e. R /\ B e. S ) /\ ( C e. R /\ D e. S ) ) -> ( E. x E. y E. z E. w ( ( <. A , B >. = <. x , y >. /\ <. C , D >. = <. z , w >. ) /\ ph ) <-> ps ) )