Metamath Proof Explorer

Theorem cotsexgw

Description: Substitution of class A for ordered triple <. x , y , z >. , analogous to copsexgw . (Contributed by BTernaryTau, 8-Sep-2026)

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

Proof

Step Hyp Ref Expression
1 vex 
 |-  x e. _V
2 vex 
 |-  y e. _V
3 vex 
 |-  z e. _V
4 1 2 3 eqvinot 
 |-  ( A = <. x , y , z >. <-> E. u E. v E. w ( A = <. u , v , w >. /\ <. u , v , w >. = <. x , y , z >. ) )
5 19.8a 
 |-  ( ( <. u , v , w >. = <. x , y , z >. /\ ph ) -> E. z ( <. u , v , w >. = <. x , y , z >. /\ ph ) )
6 5 19.8ad 
 |-  ( ( <. u , v , w >. = <. x , y , z >. /\ ph ) -> E. y E. z ( <. u , v , w >. = <. x , y , z >. /\ ph ) )
7 6 19.8ad 
 |-  ( ( <. u , v , w >. = <. x , y , z >. /\ ph ) -> E. x E. y E. z ( <. u , v , w >. = <. x , y , z >. /\ ph ) )
8 7 ex 
 |-  ( <. u , v , w >. = <. x , y , z >. -> ( ph -> E. x E. y E. z ( <. u , v , w >. = <. x , y , z >. /\ ph ) ) )
9 vex 
 |-  u e. _V
10 vex 
 |-  v e. _V
11 vex 
 |-  w e. _V
12 9 10 11 otth 
 |-  ( <. u , v , w >. = <. x , y , z >. <-> ( u = x /\ v = y /\ w = z ) )
13 12 anbi1i 
 |-  ( ( <. u , v , w >. = <. x , y , z >. /\ ph ) <-> ( ( u = x /\ v = y /\ w = z ) /\ ph ) )
14 13 3exbii 
 |-  ( E. x E. y E. z ( <. u , v , w >. = <. x , y , z >. /\ ph ) <-> E. x E. y E. z ( ( u = x /\ v = y /\ w = z ) /\ ph ) )
15 3an4anass 
 |-  ( ( ( u = x /\ v = y /\ w = z ) /\ ph ) <-> ( ( u = x /\ v = y ) /\ ( w = z /\ ph ) ) )
16 15 exbii 
 |-  ( E. z ( ( u = x /\ v = y /\ w = z ) /\ ph ) <-> E. z ( ( u = x /\ v = y ) /\ ( w = z /\ ph ) ) )
17 19.42v 
 |-  ( E. z ( ( u = x /\ v = y ) /\ ( w = z /\ ph ) ) <-> ( ( u = x /\ v = y ) /\ E. z ( w = z /\ ph ) ) )
18 16 17 bitri 
 |-  ( E. z ( ( u = x /\ v = y /\ w = z ) /\ ph ) <-> ( ( u = x /\ v = y ) /\ E. z ( w = z /\ ph ) ) )
19 18 exbii 
 |-  ( E. y E. z ( ( u = x /\ v = y /\ w = z ) /\ ph ) <-> E. y ( ( u = x /\ v = y ) /\ E. z ( w = z /\ ph ) ) )
20 anass 
 |-  ( ( ( u = x /\ v = y ) /\ E. z ( w = z /\ ph ) ) <-> ( u = x /\ ( v = y /\ E. z ( w = z /\ ph ) ) ) )
21 20 exbii 
 |-  ( E. y ( ( u = x /\ v = y ) /\ E. z ( w = z /\ ph ) ) <-> E. y ( u = x /\ ( v = y /\ E. z ( w = z /\ ph ) ) ) )
22 19.42v 
 |-  ( E. y ( u = x /\ ( v = y /\ E. z ( w = z /\ ph ) ) ) <-> ( u = x /\ E. y ( v = y /\ E. z ( w = z /\ ph ) ) ) )
23 19 21 22 3bitri 
 |-  ( E. y E. z ( ( u = x /\ v = y /\ w = z ) /\ ph ) <-> ( u = x /\ E. y ( v = y /\ E. z ( w = z /\ ph ) ) ) )
24 23 exbii 
 |-  ( E. x E. y E. z ( ( u = x /\ v = y /\ w = z ) /\ ph ) <-> E. x ( u = x /\ E. y ( v = y /\ E. z ( w = z /\ ph ) ) ) )
25 ax12ev2c 
 |-  ( u = x -> ( E. x ( u = x /\ E. y ( v = y /\ E. z ( w = z /\ ph ) ) ) -> E. y ( v = y /\ E. z ( w = z /\ ph ) ) ) )
26 ax12ev2c 
 |-  ( v = y -> ( E. y ( v = y /\ E. z ( w = z /\ ph ) ) -> E. z ( w = z /\ ph ) ) )
27 ax12ev2c 
 |-  ( w = z -> ( E. z ( w = z /\ ph ) -> ph ) )
28 26 27 sylan9 
 |-  ( ( v = y /\ w = z ) -> ( E. y ( v = y /\ E. z ( w = z /\ ph ) ) -> ph ) )
29 25 28 sylan9 
 |-  ( ( u = x /\ ( v = y /\ w = z ) ) -> ( E. x ( u = x /\ E. y ( v = y /\ E. z ( w = z /\ ph ) ) ) -> ph ) )
30 29 3impb 
 |-  ( ( u = x /\ v = y /\ w = z ) -> ( E. x ( u = x /\ E. y ( v = y /\ E. z ( w = z /\ ph ) ) ) -> ph ) )
31 24 30 biimtrid 
 |-  ( ( u = x /\ v = y /\ w = z ) -> ( E. x E. y E. z ( ( u = x /\ v = y /\ w = z ) /\ ph ) -> ph ) )
32 14 31 biimtrid 
 |-  ( ( u = x /\ v = y /\ w = z ) -> ( E. x E. y E. z ( <. u , v , w >. = <. x , y , z >. /\ ph ) -> ph ) )
33 12 32 sylbi 
 |-  ( <. u , v , w >. = <. x , y , z >. -> ( E. x E. y E. z ( <. u , v , w >. = <. x , y , z >. /\ ph ) -> ph ) )
34 8 33 impbid 
 |-  ( <. u , v , w >. = <. x , y , z >. -> ( ph <-> E. x E. y E. z ( <. u , v , w >. = <. x , y , z >. /\ ph ) ) )
35 eqeq1 
 |-  ( A = <. u , v , w >. -> ( A = <. x , y , z >. <-> <. u , v , w >. = <. x , y , z >. ) )
36 35 anbi1d 
 |-  ( A = <. u , v , w >. -> ( ( A = <. x , y , z >. /\ ph ) <-> ( <. u , v , w >. = <. x , y , z >. /\ ph ) ) )
37 36 3exbidv 
 |-  ( A = <. u , v , w >. -> ( E. x E. y E. z ( A = <. x , y , z >. /\ ph ) <-> E. x E. y E. z ( <. u , v , w >. = <. x , y , z >. /\ ph ) ) )
38 37 bibi2d 
 |-  ( A = <. u , v , w >. -> ( ( ph <-> E. x E. y E. z ( A = <. x , y , z >. /\ ph ) ) <-> ( ph <-> E. x E. y E. z ( <. u , v , w >. = <. x , y , z >. /\ ph ) ) ) )
39 35 38 imbi12d 
 |-  ( A = <. u , v , w >. -> ( ( A = <. x , y , z >. -> ( ph <-> E. x E. y E. z ( A = <. x , y , z >. /\ ph ) ) ) <-> ( <. u , v , w >. = <. x , y , z >. -> ( ph <-> E. x E. y E. z ( <. u , v , w >. = <. x , y , z >. /\ ph ) ) ) ) )
40 34 39 mpbiri 
 |-  ( A = <. u , v , w >. -> ( A = <. x , y , z >. -> ( ph <-> E. x E. y E. z ( A = <. x , y , z >. /\ ph ) ) ) )
41 40 adantr 
 |-  ( ( A = <. u , v , w >. /\ <. u , v , w >. = <. x , y , z >. ) -> ( A = <. x , y , z >. -> ( ph <-> E. x E. y E. z ( A = <. x , y , z >. /\ ph ) ) ) )
42 41 exlimiv 
 |-  ( E. w ( A = <. u , v , w >. /\ <. u , v , w >. = <. x , y , z >. ) -> ( A = <. x , y , z >. -> ( ph <-> E. x E. y E. z ( A = <. x , y , z >. /\ ph ) ) ) )
43 42 exlimivv 
 |-  ( E. u E. v E. w ( A = <. u , v , w >. /\ <. u , v , w >. = <. x , y , z >. ) -> ( A = <. x , y , z >. -> ( ph <-> E. x E. y E. z ( A = <. x , y , z >. /\ ph ) ) ) )
44 4 43 sylbi 
 |-  ( A = <. x , y , z >. -> ( A = <. x , y , z >. -> ( ph <-> E. x E. y E. z ( A = <. x , y , z >. /\ ph ) ) ) )
45 44 pm2.43i 
 |-  ( A = <. x , y , z >. -> ( ph <-> E. x E. y E. z ( A = <. x , y , z >. /\ ph ) ) )