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 ax12ev2c 
 |-  ( z = x -> ( E. x ( z = x /\ E. y ( w = y /\ ph ) ) -> E. y ( w = y /\ ph ) ) )
18 ax12ev2c 
 |-  ( w = y -> ( E. y ( w = y /\ ph ) -> ph ) )
19 17 18 sylan9 
 |-  ( ( z = x /\ w = y ) -> ( E. x ( z = x /\ E. y ( w = y /\ ph ) ) -> ph ) )
20 16 19 biimtrid 
 |-  ( ( z = x /\ w = y ) -> ( E. x E. y ( ( z = x /\ w = y ) /\ ph ) -> ph ) )
21 11 20 biimtrid 
 |-  ( ( z = x /\ w = y ) -> ( E. x E. y ( <. z , w >. = <. x , y >. /\ ph ) -> ph ) )
22 9 21 sylbi 
 |-  ( <. z , w >. = <. x , y >. -> ( E. x E. y ( <. z , w >. = <. x , y >. /\ ph ) -> ph ) )
23 6 22 impbid 
 |-  ( <. z , w >. = <. x , y >. -> ( ph <-> E. x E. y ( <. z , w >. = <. x , y >. /\ ph ) ) )
24 eqeq1 
 |-  ( A = <. z , w >. -> ( A = <. x , y >. <-> <. z , w >. = <. x , y >. ) )
25 24 anbi1d 
 |-  ( A = <. z , w >. -> ( ( A = <. x , y >. /\ ph ) <-> ( <. z , w >. = <. x , y >. /\ ph ) ) )
26 25 2exbidv 
 |-  ( A = <. z , w >. -> ( E. x E. y ( A = <. x , y >. /\ ph ) <-> E. x E. y ( <. z , w >. = <. x , y >. /\ ph ) ) )
27 26 bibi2d 
 |-  ( A = <. z , w >. -> ( ( ph <-> E. x E. y ( A = <. x , y >. /\ ph ) ) <-> ( ph <-> E. x E. y ( <. z , w >. = <. x , y >. /\ ph ) ) ) )
28 24 27 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 ) ) ) ) )
29 23 28 mpbiri 
 |-  ( A = <. z , w >. -> ( A = <. x , y >. -> ( ph <-> E. x E. y ( A = <. x , y >. /\ ph ) ) ) )
30 29 adantr 
 |-  ( ( A = <. z , w >. /\ <. z , w >. = <. x , y >. ) -> ( A = <. x , y >. -> ( ph <-> E. x E. y ( A = <. x , y >. /\ ph ) ) ) )
31 30 exlimivv 
 |-  ( E. z E. w ( A = <. z , w >. /\ <. z , w >. = <. x , y >. ) -> ( A = <. x , y >. -> ( ph <-> E. x E. y ( A = <. x , y >. /\ ph ) ) ) )
32 3 31 sylbi 
 |-  ( A = <. x , y >. -> ( A = <. x , y >. -> ( ph <-> E. x E. y ( A = <. x , y >. /\ ph ) ) ) )
33 32 pm2.43i 
 |-  ( A = <. x , y >. -> ( ph <-> E. x E. y ( A = <. x , y >. /\ ph ) ) )