Metamath Proof Explorer

Theorem copsexgw

Description: Version of copsexg with a disjoint variable condition, which does not require ax-13 . (Contributed by GG, 26-Jan-2024) Shorten proof and remove dependency on ax-10 . (Revised by Eric Schmidt, 2-May-2026)

Ref Expression
Assertion copsexgw 
|- ( 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 
 |-  ( ( <. z , w >. = <. x , y >. /\ ph ) -> E. y ( <. z , w >. = <. x , y >. /\ ph ) )
5 4 19.8ad 
 |-  ( ( <. 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 anass 
 |-  ( ( ( z = x /\ w = y ) /\ ph ) <-> ( z = x /\ ( w = y /\ ph ) ) )
13 12 exbii 
 |-  ( E. y ( ( z = x /\ w = y ) /\ ph ) <-> E. y ( z = x /\ ( w = y /\ ph ) ) )
14 19.42v 
 |-  ( E. y ( z = x /\ ( w = y /\ ph ) ) <-> ( z = x /\ E. y ( w = y /\ ph ) ) )
15 13 14 bitri 
 |-  ( E. y ( ( z = x /\ w = y ) /\ ph ) <-> ( z = x /\ E. y ( w = y /\ ph ) ) )
16 15 exbii 
 |-  ( E. x E. y ( ( z = x /\ w = y ) /\ ph ) <-> E. x ( z = x /\ E. y ( w = y /\ ph ) ) )
17 euequ 
 |-  E! x x = z
18 equcom 
 |-  ( x = z <-> z = x )
19 18 eubii 
 |-  ( E! x x = z <-> E! x z = x )
20 17 19 mpbi 
 |-  E! x z = x
21 eupick 
 |-  ( ( E! x z = x /\ E. x ( z = x /\ E. y ( w = y /\ ph ) ) ) -> ( z = x -> E. y ( w = y /\ ph ) ) )
22 20 21 mpan 
 |-  ( E. x ( z = x /\ E. y ( w = y /\ ph ) ) -> ( z = x -> E. y ( w = y /\ ph ) ) )
23 22 com12 
 |-  ( z = x -> ( E. x ( z = x /\ E. y ( w = y /\ ph ) ) -> E. y ( w = y /\ ph ) ) )
24 euequ 
 |-  E! y y = w
25 equcom 
 |-  ( y = w <-> w = y )
26 25 eubii 
 |-  ( E! y y = w <-> E! y w = y )
27 24 26 mpbi 
 |-  E! y w = y
28 eupick 
 |-  ( ( E! y w = y /\ E. y ( w = y /\ ph ) ) -> ( w = y -> ph ) )
29 27 28 mpan 
 |-  ( E. y ( w = y /\ ph ) -> ( w = y -> ph ) )
30 29 com12 
 |-  ( w = y -> ( E. y ( w = y /\ ph ) -> ph ) )
31 23 30 sylan9 
 |-  ( ( z = x /\ w = y ) -> ( E. x ( z = x /\ E. y ( w = y /\ ph ) ) -> ph ) )
32 16 31 biimtrid 
 |-  ( ( z = x /\ w = y ) -> ( E. x E. y ( ( z = x /\ w = y ) /\ ph ) -> ph ) )
33 11 32 biimtrid 
 |-  ( ( z = x /\ w = y ) -> ( E. x E. y ( <. z , w >. = <. x , y >. /\ ph ) -> ph ) )
34 9 33 sylbi 
 |-  ( <. z , w >. = <. x , y >. -> ( E. x E. y ( <. z , w >. = <. x , y >. /\ ph ) -> ph ) )
35 6 34 impbid 
 |-  ( <. z , w >. = <. x , y >. -> ( ph <-> E. x E. y ( <. z , w >. = <. x , y >. /\ ph ) ) )
36 eqeq1 
 |-  ( A = <. z , w >. -> ( A = <. x , y >. <-> <. z , w >. = <. x , y >. ) )
37 36 anbi1d 
 |-  ( A = <. z , w >. -> ( ( A = <. x , y >. /\ ph ) <-> ( <. z , w >. = <. x , y >. /\ ph ) ) )
38 37 2exbidv 
 |-  ( A = <. z , w >. -> ( E. x E. y ( A = <. x , y >. /\ ph ) <-> E. x E. y ( <. z , w >. = <. x , y >. /\ ph ) ) )
39 38 bibi2d 
 |-  ( A = <. z , w >. -> ( ( ph <-> E. x E. y ( A = <. x , y >. /\ ph ) ) <-> ( ph <-> E. x E. y ( <. z , w >. = <. x , y >. /\ ph ) ) ) )
40 36 39 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 ) ) ) ) )
41 35 40 mpbiri 
 |-  ( A = <. z , w >. -> ( A = <. x , y >. -> ( ph <-> E. x E. y ( A = <. x , y >. /\ ph ) ) ) )
42 41 adantr 
 |-  ( ( A = <. z , w >. /\ <. z , w >. = <. x , y >. ) -> ( A = <. x , y >. -> ( ph <-> E. x E. y ( A = <. x , y >. /\ ph ) ) ) )
43 42 exlimivv 
 |-  ( E. z E. w ( A = <. z , w >. /\ <. z , w >. = <. x , y >. ) -> ( A = <. x , y >. -> ( ph <-> E. x E. y ( A = <. x , y >. /\ ph ) ) ) )
44 3 43 sylbi 
 |-  ( A = <. x , y >. -> ( A = <. x , y >. -> ( ph <-> E. x E. y ( A = <. x , y >. /\ ph ) ) ) )
45 44 pm2.43i 
 |-  ( A = <. x , y >. -> ( ph <-> E. x E. y ( A = <. x , y >. /\ ph ) ) )