# Metamath Proof Explorer

## Theorem elvvv

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

Ref Expression
Assertion elvvv ${⊢}{A}\in \left(\left(\mathrm{V}×\mathrm{V}\right)×\mathrm{V}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}{A}=⟨⟨{x},{y}⟩,{z}⟩$

### Proof

Step Hyp Ref Expression
1 elxp ${⊢}{A}\in \left(\left(\mathrm{V}×\mathrm{V}\right)×\mathrm{V}\right)↔\exists {w}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({A}=⟨{w},{z}⟩\wedge \left({w}\in \left(\mathrm{V}×\mathrm{V}\right)\wedge {z}\in \mathrm{V}\right)\right)$
2 ancom ${⊢}\left({w}=⟨{x},{y}⟩\wedge {A}=⟨{w},{z}⟩\right)↔\left({A}=⟨{w},{z}⟩\wedge {w}=⟨{x},{y}⟩\right)$
3 2 2exbii ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({w}=⟨{x},{y}⟩\wedge {A}=⟨{w},{z}⟩\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({A}=⟨{w},{z}⟩\wedge {w}=⟨{x},{y}⟩\right)$
4 19.42vv ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({A}=⟨{w},{z}⟩\wedge {w}=⟨{x},{y}⟩\right)↔\left({A}=⟨{w},{z}⟩\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{w}=⟨{x},{y}⟩\right)$
5 elvv ${⊢}{w}\in \left(\mathrm{V}×\mathrm{V}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{w}=⟨{x},{y}⟩$
6 5 anbi2i ${⊢}\left({A}=⟨{w},{z}⟩\wedge {w}\in \left(\mathrm{V}×\mathrm{V}\right)\right)↔\left({A}=⟨{w},{z}⟩\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{w}=⟨{x},{y}⟩\right)$
7 vex ${⊢}{z}\in \mathrm{V}$
8 7 biantru ${⊢}\left({A}=⟨{w},{z}⟩\wedge {w}\in \left(\mathrm{V}×\mathrm{V}\right)\right)↔\left(\left({A}=⟨{w},{z}⟩\wedge {w}\in \left(\mathrm{V}×\mathrm{V}\right)\right)\wedge {z}\in \mathrm{V}\right)$
9 4 6 8 3bitr2i ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({A}=⟨{w},{z}⟩\wedge {w}=⟨{x},{y}⟩\right)↔\left(\left({A}=⟨{w},{z}⟩\wedge {w}\in \left(\mathrm{V}×\mathrm{V}\right)\right)\wedge {z}\in \mathrm{V}\right)$
10 anass ${⊢}\left(\left({A}=⟨{w},{z}⟩\wedge {w}\in \left(\mathrm{V}×\mathrm{V}\right)\right)\wedge {z}\in \mathrm{V}\right)↔\left({A}=⟨{w},{z}⟩\wedge \left({w}\in \left(\mathrm{V}×\mathrm{V}\right)\wedge {z}\in \mathrm{V}\right)\right)$
11 3 9 10 3bitrri ${⊢}\left({A}=⟨{w},{z}⟩\wedge \left({w}\in \left(\mathrm{V}×\mathrm{V}\right)\wedge {z}\in \mathrm{V}\right)\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({w}=⟨{x},{y}⟩\wedge {A}=⟨{w},{z}⟩\right)$
12 11 2exbii ${⊢}\exists {w}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({A}=⟨{w},{z}⟩\wedge \left({w}\in \left(\mathrm{V}×\mathrm{V}\right)\wedge {z}\in \mathrm{V}\right)\right)↔\exists {w}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({w}=⟨{x},{y}⟩\wedge {A}=⟨{w},{z}⟩\right)$
13 exrot4 ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨{x},{y}⟩\wedge {A}=⟨{w},{z}⟩\right)↔\exists {w}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({w}=⟨{x},{y}⟩\wedge {A}=⟨{w},{z}⟩\right)$
14 excom ${⊢}\exists {w}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨{x},{y}⟩\wedge {A}=⟨{w},{z}⟩\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}=⟨{x},{y}⟩\wedge {A}=⟨{w},{z}⟩\right)$
15 opex ${⊢}⟨{x},{y}⟩\in \mathrm{V}$
16 opeq1 ${⊢}{w}=⟨{x},{y}⟩\to ⟨{w},{z}⟩=⟨⟨{x},{y}⟩,{z}⟩$
17 16 eqeq2d ${⊢}{w}=⟨{x},{y}⟩\to \left({A}=⟨{w},{z}⟩↔{A}=⟨⟨{x},{y}⟩,{z}⟩\right)$
18 15 17 ceqsexv ${⊢}\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}=⟨{x},{y}⟩\wedge {A}=⟨{w},{z}⟩\right)↔{A}=⟨⟨{x},{y}⟩,{z}⟩$
19 18 exbii ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\left({w}=⟨{x},{y}⟩\wedge {A}=⟨{w},{z}⟩\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}{A}=⟨⟨{x},{y}⟩,{z}⟩$
20 14 19 bitri ${⊢}\exists {w}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨{x},{y}⟩\wedge {A}=⟨{w},{z}⟩\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}{A}=⟨⟨{x},{y}⟩,{z}⟩$
21 20 2exbii ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨{x},{y}⟩\wedge {A}=⟨{w},{z}⟩\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}{A}=⟨⟨{x},{y}⟩,{z}⟩$
22 12 13 21 3bitr2i ${⊢}\exists {w}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({A}=⟨{w},{z}⟩\wedge \left({w}\in \left(\mathrm{V}×\mathrm{V}\right)\wedge {z}\in \mathrm{V}\right)\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}{A}=⟨⟨{x},{y}⟩,{z}⟩$
23 1 22 bitri ${⊢}{A}\in \left(\left(\mathrm{V}×\mathrm{V}\right)×\mathrm{V}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}{A}=⟨⟨{x},{y}⟩,{z}⟩$