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 ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ → ( 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑥 ∈ V
2 vex ⊢ 𝑦 ∈ V
3 vex ⊢ 𝑧 ∈ V
4 1 2 3 eqvinot ⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ↔ ∃ 𝑢 ∃ 𝑣 ∃ 𝑤 ( 𝐴 = ⟨ 𝑢 , 𝑣 , 𝑤 ⟩ ∧ ⟨ 𝑢 , 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) )
5 19.8a ⊢ ( ( ⟨ 𝑢 , 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) → ∃ 𝑧 ( ⟨ 𝑢 , 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) )
6 5 19.8ad ⊢ ( ( ⟨ 𝑢 , 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) → ∃ 𝑦 ∃ 𝑧 ( ⟨ 𝑢 , 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) )
7 6 19.8ad ⊢ ( ( ⟨ 𝑢 , 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) → ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ⟨ 𝑢 , 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) )
8 7 ex ⊢ ( ⟨ 𝑢 , 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ → ( 𝜑 → ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ⟨ 𝑢 , 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) ) )
9 vex ⊢ 𝑢 ∈ V
10 vex ⊢ 𝑣 ∈ V
11 vex ⊢ 𝑤 ∈ V
12 9 10 11 otth ⊢ ( ⟨ 𝑢 , 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ↔ ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑦 ∧ 𝑤 = 𝑧 ) )
13 12 anbi1i ⊢ ( ( ⟨ 𝑢 , 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) ↔ ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑦 ∧ 𝑤 = 𝑧 ) ∧ 𝜑 ) )
14 13 3exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ⟨ 𝑢 , 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑦 ∧ 𝑤 = 𝑧 ) ∧ 𝜑 ) )
15 3an4anass ⊢ ( ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑦 ∧ 𝑤 = 𝑧 ) ∧ 𝜑 ) ↔ ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑦 ) ∧ ( 𝑤 = 𝑧 ∧ 𝜑 ) ) )
16 15 exbii ⊢ ( ∃ 𝑧 ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑦 ∧ 𝑤 = 𝑧 ) ∧ 𝜑 ) ↔ ∃ 𝑧 ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑦 ) ∧ ( 𝑤 = 𝑧 ∧ 𝜑 ) ) )
17 19.42v ⊢ ( ∃ 𝑧 ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑦 ) ∧ ( 𝑤 = 𝑧 ∧ 𝜑 ) ) ↔ ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑦 ) ∧ ∃ 𝑧 ( 𝑤 = 𝑧 ∧ 𝜑 ) ) )
18 16 17 bitri ⊢ ( ∃ 𝑧 ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑦 ∧ 𝑤 = 𝑧 ) ∧ 𝜑 ) ↔ ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑦 ) ∧ ∃ 𝑧 ( 𝑤 = 𝑧 ∧ 𝜑 ) ) )
19 18 exbii ⊢ ( ∃ 𝑦 ∃ 𝑧 ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑦 ∧ 𝑤 = 𝑧 ) ∧ 𝜑 ) ↔ ∃ 𝑦 ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑦 ) ∧ ∃ 𝑧 ( 𝑤 = 𝑧 ∧ 𝜑 ) ) )
20 anass ⊢ ( ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑦 ) ∧ ∃ 𝑧 ( 𝑤 = 𝑧 ∧ 𝜑 ) ) ↔ ( 𝑢 = 𝑥 ∧ ( 𝑣 = 𝑦 ∧ ∃ 𝑧 ( 𝑤 = 𝑧 ∧ 𝜑 ) ) ) )
21 20 exbii ⊢ ( ∃ 𝑦 ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑦 ) ∧ ∃ 𝑧 ( 𝑤 = 𝑧 ∧ 𝜑 ) ) ↔ ∃ 𝑦 ( 𝑢 = 𝑥 ∧ ( 𝑣 = 𝑦 ∧ ∃ 𝑧 ( 𝑤 = 𝑧 ∧ 𝜑 ) ) ) )
22 19.42v ⊢ ( ∃ 𝑦 ( 𝑢 = 𝑥 ∧ ( 𝑣 = 𝑦 ∧ ∃ 𝑧 ( 𝑤 = 𝑧 ∧ 𝜑 ) ) ) ↔ ( 𝑢 = 𝑥 ∧ ∃ 𝑦 ( 𝑣 = 𝑦 ∧ ∃ 𝑧 ( 𝑤 = 𝑧 ∧ 𝜑 ) ) ) )
23 19 21 22 3bitri ⊢ ( ∃ 𝑦 ∃ 𝑧 ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑦 ∧ 𝑤 = 𝑧 ) ∧ 𝜑 ) ↔ ( 𝑢 = 𝑥 ∧ ∃ 𝑦 ( 𝑣 = 𝑦 ∧ ∃ 𝑧 ( 𝑤 = 𝑧 ∧ 𝜑 ) ) ) )
24 23 exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑦 ∧ 𝑤 = 𝑧 ) ∧ 𝜑 ) ↔ ∃ 𝑥 ( 𝑢 = 𝑥 ∧ ∃ 𝑦 ( 𝑣 = 𝑦 ∧ ∃ 𝑧 ( 𝑤 = 𝑧 ∧ 𝜑 ) ) ) )
25 ax12ev2c ⊢ ( 𝑢 = 𝑥 → ( ∃ 𝑥 ( 𝑢 = 𝑥 ∧ ∃ 𝑦 ( 𝑣 = 𝑦 ∧ ∃ 𝑧 ( 𝑤 = 𝑧 ∧ 𝜑 ) ) ) → ∃ 𝑦 ( 𝑣 = 𝑦 ∧ ∃ 𝑧 ( 𝑤 = 𝑧 ∧ 𝜑 ) ) ) )
26 ax12ev2c ⊢ ( 𝑣 = 𝑦 → ( ∃ 𝑦 ( 𝑣 = 𝑦 ∧ ∃ 𝑧 ( 𝑤 = 𝑧 ∧ 𝜑 ) ) → ∃ 𝑧 ( 𝑤 = 𝑧 ∧ 𝜑 ) ) )
27 ax12ev2c ⊢ ( 𝑤 = 𝑧 → ( ∃ 𝑧 ( 𝑤 = 𝑧 ∧ 𝜑 ) → 𝜑 ) )
28 26 27 sylan9 ⊢ ( ( 𝑣 = 𝑦 ∧ 𝑤 = 𝑧 ) → ( ∃ 𝑦 ( 𝑣 = 𝑦 ∧ ∃ 𝑧 ( 𝑤 = 𝑧 ∧ 𝜑 ) ) → 𝜑 ) )
29 25 28 sylan9 ⊢ ( ( 𝑢 = 𝑥 ∧ ( 𝑣 = 𝑦 ∧ 𝑤 = 𝑧 ) ) → ( ∃ 𝑥 ( 𝑢 = 𝑥 ∧ ∃ 𝑦 ( 𝑣 = 𝑦 ∧ ∃ 𝑧 ( 𝑤 = 𝑧 ∧ 𝜑 ) ) ) → 𝜑 ) )
30 29 3impb ⊢ ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑦 ∧ 𝑤 = 𝑧 ) → ( ∃ 𝑥 ( 𝑢 = 𝑥 ∧ ∃ 𝑦 ( 𝑣 = 𝑦 ∧ ∃ 𝑧 ( 𝑤 = 𝑧 ∧ 𝜑 ) ) ) → 𝜑 ) )
31 24 30 biimtrid ⊢ ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑦 ∧ 𝑤 = 𝑧 ) → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑦 ∧ 𝑤 = 𝑧 ) ∧ 𝜑 ) → 𝜑 ) )
32 14 31 biimtrid ⊢ ( ( 𝑢 = 𝑥 ∧ 𝑣 = 𝑦 ∧ 𝑤 = 𝑧 ) → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ⟨ 𝑢 , 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) → 𝜑 ) )
33 12 32 sylbi ⊢ ( ⟨ 𝑢 , 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ⟨ 𝑢 , 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) → 𝜑 ) )
34 8 33 impbid ⊢ ( ⟨ 𝑢 , 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ → ( 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ⟨ 𝑢 , 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) ) )
35 eqeq1 ⊢ ( 𝐴 = ⟨ 𝑢 , 𝑣 , 𝑤 ⟩ → ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ↔ ⟨ 𝑢 , 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) )
36 35 anbi1d ⊢ ( 𝐴 = ⟨ 𝑢 , 𝑣 , 𝑤 ⟩ → ( ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) ↔ ( ⟨ 𝑢 , 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) ) )
37 36 3exbidv ⊢ ( 𝐴 = ⟨ 𝑢 , 𝑣 , 𝑤 ⟩ → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ⟨ 𝑢 , 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) ) )
38 37 bibi2d ⊢ ( 𝐴 = ⟨ 𝑢 , 𝑣 , 𝑤 ⟩ → ( ( 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) ) ↔ ( 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ⟨ 𝑢 , 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) ) ) )
39 35 38 imbi12d ⊢ ( 𝐴 = ⟨ 𝑢 , 𝑣 , 𝑤 ⟩ → ( ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ → ( 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) ) ) ↔ ( ⟨ 𝑢 , 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ → ( 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ⟨ 𝑢 , 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) ) ) ) )
40 34 39 mpbiri ⊢ ( 𝐴 = ⟨ 𝑢 , 𝑣 , 𝑤 ⟩ → ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ → ( 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) ) ) )
41 40 adantr ⊢ ( ( 𝐴 = ⟨ 𝑢 , 𝑣 , 𝑤 ⟩ ∧ ⟨ 𝑢 , 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) → ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ → ( 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) ) ) )
42 41 exlimiv ⊢ ( ∃ 𝑤 ( 𝐴 = ⟨ 𝑢 , 𝑣 , 𝑤 ⟩ ∧ ⟨ 𝑢 , 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) → ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ → ( 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) ) ) )
43 42 exlimivv ⊢ ( ∃ 𝑢 ∃ 𝑣 ∃ 𝑤 ( 𝐴 = ⟨ 𝑢 , 𝑣 , 𝑤 ⟩ ∧ ⟨ 𝑢 , 𝑣 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) → ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ → ( 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) ) ) )
44 4 43 sylbi ⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ → ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ → ( 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) ) ) )
45 44 pm2.43i ⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ → ( 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ 𝜑 ) ) )