Metamath Proof Explorer

Theorem copsexg

Description: Substitution of class A for ordered pair <. x , y >. . Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker copsexgw when possible. (Contributed by NM, 27-Dec-1996) (Revised by Andrew Salmon, 11-Jul-2011) (Proof shortened by Wolf Lammen, 25-Aug-2019) (New usage is discouraged.)

Ref Expression
Assertion copsexg 
|- ( A = <. x , y >. -> ( ph <-> E. x E. y ( A = <. x , y >. /\ ph ) ) )

Proof

Step Hyp Ref Expression
1 vex 
 |-  x e. _V
2 vex 
 |-  y e. _V
3 1 2 eqvinop 
 |-  ( A = <. x , y >. <-> E. z E. w ( A = <. z , w >. /\ <. z , w >. = <. x , y >. ) )
4 19.8a 
 |-  ( E. y ( <. z , w >. = <. x , y >. /\ ph ) -> E. x E. y ( <. z , w >. = <. x , y >. /\ ph ) )
5 4 19.23bi 
 |-  ( ( <. z , w >. = <. x , y >. /\ ph ) -> E. x E. y ( <. z , w >. = <. x , y >. /\ ph ) )
6 5 ex 
 |-  ( <. z , w >. = <. x , y >. -> ( ph -> E. x E. y ( <. z , w >. = <. x , y >. /\ ph ) ) )
7 vex 
 |-  z e. _V
8 vex 
 |-  w e. _V
9 7 8 opth 
 |-  ( <. z , w >. = <. x , y >. <-> ( z = x /\ w = y ) )
10 9 anbi1i 
 |-  ( ( <. z , w >. = <. x , y >. /\ ph ) <-> ( ( z = x /\ w = y ) /\ ph ) )
11 10 2exbii 
 |-  ( E. x E. y ( <. z , w >. = <. x , y >. /\ ph ) <-> E. x E. y ( ( z = x /\ w = y ) /\ ph ) )
12 nfe1 
 |-  F/ x E. x ( z = x /\ E. y ( w = y /\ ph ) )
13 19.8a 
 |-  ( ( w = y /\ ph ) -> E. y ( w = y /\ ph ) )
14 13 anim2i 
 |-  ( ( z = x /\ ( w = y /\ ph ) ) -> ( z = x /\ E. y ( w = y /\ ph ) ) )
15 14 anassrs 
 |-  ( ( ( z = x /\ w = y ) /\ ph ) -> ( z = x /\ E. y ( w = y /\ ph ) ) )
16 15 eximi 
 |-  ( E. y ( ( z = x /\ w = y ) /\ ph ) -> E. y ( z = x /\ E. y ( w = y /\ ph ) ) )
17 biidd 
 |-  ( A. y y = x -> ( ( z = x /\ E. y ( w = y /\ ph ) ) <-> ( z = x /\ E. y ( w = y /\ ph ) ) ) )
18 17 drex1 
 |-  ( A. y y = x -> ( E. y ( z = x /\ E. y ( w = y /\ ph ) ) <-> E. x ( z = x /\ E. y ( w = y /\ ph ) ) ) )
19 16 18 syl5ib 
 |-  ( A. y y = x -> ( E. y ( ( z = x /\ w = y ) /\ ph ) -> E. x ( z = x /\ E. y ( w = y /\ ph ) ) ) )
20 anass 
 |-  ( ( ( z = x /\ w = y ) /\ ph ) <-> ( z = x /\ ( w = y /\ ph ) ) )
21 20 exbii 
 |-  ( E. y ( ( z = x /\ w = y ) /\ ph ) <-> E. y ( z = x /\ ( w = y /\ ph ) ) )
22 19.40 
 |-  ( E. y ( z = x /\ ( w = y /\ ph ) ) -> ( E. y z = x /\ E. y ( w = y /\ ph ) ) )
23 nfeqf2 
 |-  ( -. A. y y = x -> F/ y z = x )
24 23 19.9d 
 |-  ( -. A. y y = x -> ( E. y z = x -> z = x ) )
25 24 anim1d 
 |-  ( -. A. y y = x -> ( ( E. y z = x /\ E. y ( w = y /\ ph ) ) -> ( z = x /\ E. y ( w = y /\ ph ) ) ) )
26 22 25 syl5 
 |-  ( -. A. y y = x -> ( E. y ( z = x /\ ( w = y /\ ph ) ) -> ( z = x /\ E. y ( w = y /\ ph ) ) ) )
27 21 26 syl5bi 
 |-  ( -. A. y y = x -> ( E. y ( ( z = x /\ w = y ) /\ ph ) -> ( z = x /\ E. y ( w = y /\ ph ) ) ) )
28 19.8a 
 |-  ( ( z = x /\ E. y ( w = y /\ ph ) ) -> E. x ( z = x /\ E. y ( w = y /\ ph ) ) )
29 27 28 syl6 
 |-  ( -. A. y y = x -> ( E. y ( ( z = x /\ w = y ) /\ ph ) -> E. x ( z = x /\ E. y ( w = y /\ ph ) ) ) )
30 19 29 pm2.61i 
 |-  ( E. y ( ( z = x /\ w = y ) /\ ph ) -> E. x ( z = x /\ E. y ( w = y /\ ph ) ) )
31 12 30 exlimi 
 |-  ( E. x E. y ( ( z = x /\ w = y ) /\ ph ) -> E. x ( z = x /\ E. y ( w = y /\ ph ) ) )
32 euequ 
 |-  E! x x = z
33 equcom 
 |-  ( x = z <-> z = x )
34 33 eubii 
 |-  ( E! x x = z <-> E! x z = x )
35 32 34 mpbi 
 |-  E! x z = x
36 eupick 
 |-  ( ( E! x z = x /\ E. x ( z = x /\ E. y ( w = y /\ ph ) ) ) -> ( z = x -> E. y ( w = y /\ ph ) ) )
37 35 36 mpan 
 |-  ( E. x ( z = x /\ E. y ( w = y /\ ph ) ) -> ( z = x -> E. y ( w = y /\ ph ) ) )
38 37 com12 
 |-  ( z = x -> ( E. x ( z = x /\ E. y ( w = y /\ ph ) ) -> E. y ( w = y /\ ph ) ) )
39 euequ 
 |-  E! y y = w
40 equcom 
 |-  ( y = w <-> w = y )
41 40 eubii 
 |-  ( E! y y = w <-> E! y w = y )
42 39 41 mpbi 
 |-  E! y w = y
43 eupick 
 |-  ( ( E! y w = y /\ E. y ( w = y /\ ph ) ) -> ( w = y -> ph ) )
44 42 43 mpan 
 |-  ( E. y ( w = y /\ ph ) -> ( w = y -> ph ) )
45 44 com12 
 |-  ( w = y -> ( E. y ( w = y /\ ph ) -> ph ) )
46 38 45 sylan9 
 |-  ( ( z = x /\ w = y ) -> ( E. x ( z = x /\ E. y ( w = y /\ ph ) ) -> ph ) )
47 31 46 syl5 
 |-  ( ( z = x /\ w = y ) -> ( E. x E. y ( ( z = x /\ w = y ) /\ ph ) -> ph ) )
48 11 47 syl5bi 
 |-  ( ( z = x /\ w = y ) -> ( E. x E. y ( <. z , w >. = <. x , y >. /\ ph ) -> ph ) )
49 9 48 sylbi 
 |-  ( <. z , w >. = <. x , y >. -> ( E. x E. y ( <. z , w >. = <. x , y >. /\ ph ) -> ph ) )
50 6 49 impbid 
 |-  ( <. z , w >. = <. x , y >. -> ( ph <-> E. x E. y ( <. z , w >. = <. x , y >. /\ ph ) ) )
51 eqeq1 
 |-  ( A = <. z , w >. -> ( A = <. x , y >. <-> <. z , w >. = <. x , y >. ) )
52 51 anbi1d 
 |-  ( A = <. z , w >. -> ( ( A = <. x , y >. /\ ph ) <-> ( <. z , w >. = <. x , y >. /\ ph ) ) )
53 52 2exbidv 
 |-  ( A = <. z , w >. -> ( E. x E. y ( A = <. x , y >. /\ ph ) <-> E. x E. y ( <. z , w >. = <. x , y >. /\ ph ) ) )
54 53 bibi2d 
 |-  ( A = <. z , w >. -> ( ( ph <-> E. x E. y ( A = <. x , y >. /\ ph ) ) <-> ( ph <-> E. x E. y ( <. z , w >. = <. x , y >. /\ ph ) ) ) )
55 51 54 imbi12d 
 |-  ( A = <. z , w >. -> ( ( A = <. x , y >. -> ( ph <-> E. x E. y ( A = <. x , y >. /\ ph ) ) ) <-> ( <. z , w >. = <. x , y >. -> ( ph <-> E. x E. y ( <. z , w >. = <. x , y >. /\ ph ) ) ) ) )
56 50 55 mpbiri 
 |-  ( A = <. z , w >. -> ( A = <. x , y >. -> ( ph <-> E. x E. y ( A = <. x , y >. /\ ph ) ) ) )
57 56 adantr 
 |-  ( ( A = <. z , w >. /\ <. z , w >. = <. x , y >. ) -> ( A = <. x , y >. -> ( ph <-> E. x E. y ( A = <. x , y >. /\ ph ) ) ) )
58 57 exlimivv 
 |-  ( E. z E. w ( A = <. z , w >. /\ <. z , w >. = <. x , y >. ) -> ( A = <. x , y >. -> ( ph <-> E. x E. y ( A = <. x , y >. /\ ph ) ) ) )
59 3 58 sylbi 
 |-  ( A = <. x , y >. -> ( A = <. x , y >. -> ( ph <-> E. x E. y ( A = <. x , y >. /\ ph ) ) ) )
60 59 pm2.43i 
 |-  ( A = <. x , y >. -> ( ph <-> E. x E. y ( A = <. x , y >. /\ ph ) ) )