Metamath Proof Explorer

Theorem copsex2gOLD

Description: Obsolete version of copsex2g as of 1-Sep-2024. (Contributed by NM, 28-May-1995) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis copsex2g.1 
|- ( ( x = A /\ y = B ) -> ( ph <-> ps ) )
Assertion copsex2gOLD 
|- ( ( 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 elisset 
 |-  ( A e. V -> E. x x = A )
3 elisset 
 |-  ( B e. W -> E. y y = B )
4 exdistrv 
 |-  ( E. x E. y ( x = A /\ y = B ) <-> ( E. x x = A /\ E. y y = B ) )
5 nfe1 
 |-  F/ x E. x E. y ( <. A , B >. = <. x , y >. /\ ph )
6 nfv 
 |-  F/ x ps
7 5 6 nfbi 
 |-  F/ x ( E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) <-> ps )
8 nfe1 
 |-  F/ y E. y ( <. A , B >. = <. x , y >. /\ ph )
9 8 nfex 
 |-  F/ y E. x E. y ( <. A , B >. = <. x , y >. /\ ph )
10 nfv 
 |-  F/ y ps
11 9 10 nfbi 
 |-  F/ y ( E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) <-> ps )
12 opeq12 
 |-  ( ( x = A /\ y = B ) -> <. x , y >. = <. A , B >. )
13 copsexgw 
 |-  ( <. A , B >. = <. x , y >. -> ( ph <-> E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) ) )
14 13 eqcoms 
 |-  ( <. x , y >. = <. A , B >. -> ( ph <-> E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) ) )
15 12 14 syl 
 |-  ( ( x = A /\ y = B ) -> ( ph <-> E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) ) )
16 15 1 bitr3d 
 |-  ( ( x = A /\ y = B ) -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) <-> ps ) )
17 11 16 exlimi 
 |-  ( E. y ( x = A /\ y = B ) -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) <-> ps ) )
18 7 17 exlimi 
 |-  ( E. x E. y ( x = A /\ y = B ) -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) <-> ps ) )
19 4 18 sylbir 
 |-  ( ( E. x x = A /\ E. y y = B ) -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) <-> ps ) )
20 2 3 19 syl2an 
 |-  ( ( A e. V /\ B e. W ) -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) <-> ps ) )