This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elvvv

Description: Membership in universal class of ordered triples. (Contributed by NM, 17-Dec-2008)

Ref Expression
Assertion elvvv ( 𝐴 ∈ ( ( V × V ) × V ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )

Proof

Step Hyp Ref Expression
1 elxp ⊢ ( 𝐴 ∈ ( ( V × V ) × V ) ↔ ∃ 𝑤 ∃ 𝑧 ( 𝐴 = ⟨ 𝑤 , 𝑧 ⟩ ∧ ( 𝑤 ∈ ( V × V ) ∧ 𝑧 ∈ V ) ) )
2 ancom ⊢ ( ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 = ⟨ 𝑤 , 𝑧 ⟩ ) ↔ ( 𝐴 = ⟨ 𝑤 , 𝑧 ⟩ ∧ 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ) )
3 2 2exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 = ⟨ 𝑤 , 𝑧 ⟩ ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑤 , 𝑧 ⟩ ∧ 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ) )
4 19.42vv ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑤 , 𝑧 ⟩ ∧ 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( 𝐴 = ⟨ 𝑤 , 𝑧 ⟩ ∧ ∃ 𝑥 ∃ 𝑦 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ) )
5 elvv ⊢ ( 𝑤 ∈ ( V × V ) ↔ ∃ 𝑥 ∃ 𝑦 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ )
6 5 anbi2i ⊢ ( ( 𝐴 = ⟨ 𝑤 , 𝑧 ⟩ ∧ 𝑤 ∈ ( V × V ) ) ↔ ( 𝐴 = ⟨ 𝑤 , 𝑧 ⟩ ∧ ∃ 𝑥 ∃ 𝑦 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ) )
7 vex ⊢ 𝑧 ∈ V
8 7 biantru ⊢ ( ( 𝐴 = ⟨ 𝑤 , 𝑧 ⟩ ∧ 𝑤 ∈ ( V × V ) ) ↔ ( ( 𝐴 = ⟨ 𝑤 , 𝑧 ⟩ ∧ 𝑤 ∈ ( V × V ) ) ∧ 𝑧 ∈ V ) )
9 4 6 8 3bitr2i ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑤 , 𝑧 ⟩ ∧ 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( ( 𝐴 = ⟨ 𝑤 , 𝑧 ⟩ ∧ 𝑤 ∈ ( V × V ) ) ∧ 𝑧 ∈ V ) )
10 anass ⊢ ( ( ( 𝐴 = ⟨ 𝑤 , 𝑧 ⟩ ∧ 𝑤 ∈ ( V × V ) ) ∧ 𝑧 ∈ V ) ↔ ( 𝐴 = ⟨ 𝑤 , 𝑧 ⟩ ∧ ( 𝑤 ∈ ( V × V ) ∧ 𝑧 ∈ V ) ) )
11 3 9 10 3bitrri ⊢ ( ( 𝐴 = ⟨ 𝑤 , 𝑧 ⟩ ∧ ( 𝑤 ∈ ( V × V ) ∧ 𝑧 ∈ V ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 = ⟨ 𝑤 , 𝑧 ⟩ ) )
12 11 2exbii ⊢ ( ∃ 𝑤 ∃ 𝑧 ( 𝐴 = ⟨ 𝑤 , 𝑧 ⟩ ∧ ( 𝑤 ∈ ( V × V ) ∧ 𝑧 ∈ V ) ) ↔ ∃ 𝑤 ∃ 𝑧 ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 = ⟨ 𝑤 , 𝑧 ⟩ ) )
13 exrot4 ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑤 ∃ 𝑧 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 = ⟨ 𝑤 , 𝑧 ⟩ ) ↔ ∃ 𝑤 ∃ 𝑧 ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 = ⟨ 𝑤 , 𝑧 ⟩ ) )
14 excom ⊢ ( ∃ 𝑤 ∃ 𝑧 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 = ⟨ 𝑤 , 𝑧 ⟩ ) ↔ ∃ 𝑧 ∃ 𝑤 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 = ⟨ 𝑤 , 𝑧 ⟩ ) )
15 opex ⊢ ⟨ 𝑥 , 𝑦 ⟩ ∈ V
16 opeq1 ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ⟨ 𝑤 , 𝑧 ⟩ = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )
17 16 eqeq2d ⊢ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐴 = ⟨ 𝑤 , 𝑧 ⟩ ↔ 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) )
18 15 17 ceqsexv ⊢ ( ∃ 𝑤 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 = ⟨ 𝑤 , 𝑧 ⟩ ) ↔ 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )
19 18 exbii ⊢ ( ∃ 𝑧 ∃ 𝑤 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 = ⟨ 𝑤 , 𝑧 ⟩ ) ↔ ∃ 𝑧 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )
20 14 19 bitri ⊢ ( ∃ 𝑤 ∃ 𝑧 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 = ⟨ 𝑤 , 𝑧 ⟩ ) ↔ ∃ 𝑧 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )
21 20 2exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑤 ∃ 𝑧 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 = ⟨ 𝑤 , 𝑧 ⟩ ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )
22 12 13 21 3bitr2i ⊢ ( ∃ 𝑤 ∃ 𝑧 ( 𝐴 = ⟨ 𝑤 , 𝑧 ⟩ ∧ ( 𝑤 ∈ ( V × V ) ∧ 𝑧 ∈ V ) ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )
23 1 22 bitri ⊢ ( 𝐴 ∈ ( ( V × V ) × V ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )