Metamath Proof Explorer

Theorem eqvinot

Description: A variable introduction law for ordered triples, analogous to eqvinop . (Contributed by BTernaryTau, 8-Sep-2026)

Ref Expression
Hypotheses eqvinot.1 ⊢ 𝐵 ∈ V
eqvinot.2 ⊢ 𝐶 ∈ V
eqvinot.3 ⊢ 𝐷 ∈ V
Assertion eqvinot ( 𝐴 = ⟨ 𝐵 , 𝐶 , 𝐷 ⟩ ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ = ⟨ 𝐵 , 𝐶 , 𝐷 ⟩ ) )

Proof

Step Hyp Ref Expression
1 eqvinot.1 ⊢ 𝐵 ∈ V
2 eqvinot.2 ⊢ 𝐶 ∈ V
3 eqvinot.3 ⊢ 𝐷 ∈ V
4 19.42v ⊢ ( ∃ 𝑦 ( 𝑥 = 𝐵 ∧ ( 𝑦 = 𝐶 ∧ 𝐴 = ⟨ 𝑥 , 𝑦 , 𝐷 ⟩ ) ) ↔ ( 𝑥 = 𝐵 ∧ ∃ 𝑦 ( 𝑦 = 𝐶 ∧ 𝐴 = ⟨ 𝑥 , 𝑦 , 𝐷 ⟩ ) ) )
5 19.42v ⊢ ( ∃ 𝑧 ( ( 𝑥 = 𝐵 ∧ 𝑦 = 𝐶 ) ∧ ( 𝑧 = 𝐷 ∧ 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) ) ↔ ( ( 𝑥 = 𝐵 ∧ 𝑦 = 𝐶 ) ∧ ∃ 𝑧 ( 𝑧 = 𝐷 ∧ 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) ) )
6 vex ⊢ 𝑥 ∈ V
7 vex ⊢ 𝑦 ∈ V
8 vex ⊢ 𝑧 ∈ V
9 6 7 8 otth ⊢ ( ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ = ⟨ 𝐵 , 𝐶 , 𝐷 ⟩ ↔ ( 𝑥 = 𝐵 ∧ 𝑦 = 𝐶 ∧ 𝑧 = 𝐷 ) )
10 9 anbi2i ⊢ ( ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ = ⟨ 𝐵 , 𝐶 , 𝐷 ⟩ ) ↔ ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( 𝑥 = 𝐵 ∧ 𝑦 = 𝐶 ∧ 𝑧 = 𝐷 ) ) )
11 ancom ⊢ ( ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ( 𝑥 = 𝐵 ∧ 𝑦 = 𝐶 ∧ 𝑧 = 𝐷 ) ) ↔ ( ( 𝑥 = 𝐵 ∧ 𝑦 = 𝐶 ∧ 𝑧 = 𝐷 ) ∧ 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) )
12 3an4anass ⊢ ( ( ( 𝑥 = 𝐵 ∧ 𝑦 = 𝐶 ∧ 𝑧 = 𝐷 ) ∧ 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) ↔ ( ( 𝑥 = 𝐵 ∧ 𝑦 = 𝐶 ) ∧ ( 𝑧 = 𝐷 ∧ 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) ) )
13 10 11 12 3bitrri ⊢ ( ( ( 𝑥 = 𝐵 ∧ 𝑦 = 𝐶 ) ∧ ( 𝑧 = 𝐷 ∧ 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) ) ↔ ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ = ⟨ 𝐵 , 𝐶 , 𝐷 ⟩ ) )
14 13 exbii ⊢ ( ∃ 𝑧 ( ( 𝑥 = 𝐵 ∧ 𝑦 = 𝐶 ) ∧ ( 𝑧 = 𝐷 ∧ 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) ) ↔ ∃ 𝑧 ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ = ⟨ 𝐵 , 𝐶 , 𝐷 ⟩ ) )
15 oteq3 ⊢ ( 𝑧 = 𝐷 → ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ = ⟨ 𝑥 , 𝑦 , 𝐷 ⟩ )
16 15 eqeq2d ⊢ ( 𝑧 = 𝐷 → ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ↔ 𝐴 = ⟨ 𝑥 , 𝑦 , 𝐷 ⟩ ) )
17 3 16 ceqsexv ⊢ ( ∃ 𝑧 ( 𝑧 = 𝐷 ∧ 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) ↔ 𝐴 = ⟨ 𝑥 , 𝑦 , 𝐷 ⟩ )
18 17 anbi2i ⊢ ( ( ( 𝑥 = 𝐵 ∧ 𝑦 = 𝐶 ) ∧ ∃ 𝑧 ( 𝑧 = 𝐷 ∧ 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) ) ↔ ( ( 𝑥 = 𝐵 ∧ 𝑦 = 𝐶 ) ∧ 𝐴 = ⟨ 𝑥 , 𝑦 , 𝐷 ⟩ ) )
19 5 14 18 3bitr3i ⊢ ( ∃ 𝑧 ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ = ⟨ 𝐵 , 𝐶 , 𝐷 ⟩ ) ↔ ( ( 𝑥 = 𝐵 ∧ 𝑦 = 𝐶 ) ∧ 𝐴 = ⟨ 𝑥 , 𝑦 , 𝐷 ⟩ ) )
20 anass ⊢ ( ( ( 𝑥 = 𝐵 ∧ 𝑦 = 𝐶 ) ∧ 𝐴 = ⟨ 𝑥 , 𝑦 , 𝐷 ⟩ ) ↔ ( 𝑥 = 𝐵 ∧ ( 𝑦 = 𝐶 ∧ 𝐴 = ⟨ 𝑥 , 𝑦 , 𝐷 ⟩ ) ) )
21 19 20 bitr2i ⊢ ( ( 𝑥 = 𝐵 ∧ ( 𝑦 = 𝐶 ∧ 𝐴 = ⟨ 𝑥 , 𝑦 , 𝐷 ⟩ ) ) ↔ ∃ 𝑧 ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ = ⟨ 𝐵 , 𝐶 , 𝐷 ⟩ ) )
22 21 exbii ⊢ ( ∃ 𝑦 ( 𝑥 = 𝐵 ∧ ( 𝑦 = 𝐶 ∧ 𝐴 = ⟨ 𝑥 , 𝑦 , 𝐷 ⟩ ) ) ↔ ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ = ⟨ 𝐵 , 𝐶 , 𝐷 ⟩ ) )
23 oteq2 ⊢ ( 𝑦 = 𝐶 → ⟨ 𝑥 , 𝑦 , 𝐷 ⟩ = ⟨ 𝑥 , 𝐶 , 𝐷 ⟩ )
24 23 eqeq2d ⊢ ( 𝑦 = 𝐶 → ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝐷 ⟩ ↔ 𝐴 = ⟨ 𝑥 , 𝐶 , 𝐷 ⟩ ) )
25 2 24 ceqsexv ⊢ ( ∃ 𝑦 ( 𝑦 = 𝐶 ∧ 𝐴 = ⟨ 𝑥 , 𝑦 , 𝐷 ⟩ ) ↔ 𝐴 = ⟨ 𝑥 , 𝐶 , 𝐷 ⟩ )
26 25 anbi2i ⊢ ( ( 𝑥 = 𝐵 ∧ ∃ 𝑦 ( 𝑦 = 𝐶 ∧ 𝐴 = ⟨ 𝑥 , 𝑦 , 𝐷 ⟩ ) ) ↔ ( 𝑥 = 𝐵 ∧ 𝐴 = ⟨ 𝑥 , 𝐶 , 𝐷 ⟩ ) )
27 4 22 26 3bitr3i ⊢ ( ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ = ⟨ 𝐵 , 𝐶 , 𝐷 ⟩ ) ↔ ( 𝑥 = 𝐵 ∧ 𝐴 = ⟨ 𝑥 , 𝐶 , 𝐷 ⟩ ) )
28 27 exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ = ⟨ 𝐵 , 𝐶 , 𝐷 ⟩ ) ↔ ∃ 𝑥 ( 𝑥 = 𝐵 ∧ 𝐴 = ⟨ 𝑥 , 𝐶 , 𝐷 ⟩ ) )
29 oteq1 ⊢ ( 𝑥 = 𝐵 → ⟨ 𝑥 , 𝐶 , 𝐷 ⟩ = ⟨ 𝐵 , 𝐶 , 𝐷 ⟩ )
30 29 eqeq2d ⊢ ( 𝑥 = 𝐵 → ( 𝐴 = ⟨ 𝑥 , 𝐶 , 𝐷 ⟩ ↔ 𝐴 = ⟨ 𝐵 , 𝐶 , 𝐷 ⟩ ) )
31 1 30 ceqsexv ⊢ ( ∃ 𝑥 ( 𝑥 = 𝐵 ∧ 𝐴 = ⟨ 𝑥 , 𝐶 , 𝐷 ⟩ ) ↔ 𝐴 = ⟨ 𝐵 , 𝐶 , 𝐷 ⟩ )
32 28 31 bitr2i ⊢ ( 𝐴 = ⟨ 𝐵 , 𝐶 , 𝐷 ⟩ ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ∧ ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ = ⟨ 𝐵 , 𝐶 , 𝐷 ⟩ ) )