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