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}\times \mathrm{V}\right)\times \mathrm{V}\right)\leftrightarrow \exists x\exists y\exists zA=⟨⟨x,y⟩,z⟩$$

Proof

Step	Hyp	Ref	Expression
1		elxp	$$⊢A\in \left(\left(\mathrm{V}\times \mathrm{V}\right)\times \mathrm{V}\right)\leftrightarrow \exists w\exists z\left(A=⟨w,z⟩\wedge \left(w\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge z\in \mathrm{V}\right)\right)$$
2		ancom	$$⊢\left(w=⟨x,y⟩\wedge A=⟨w,z⟩\right)\leftrightarrow \left(A=⟨w,z⟩\wedge w=⟨x,y⟩\right)$$
3	2	2exbii	$$⊢\exists x\exists y\left(w=⟨x,y⟩\wedge A=⟨w,z⟩\right)\leftrightarrow \exists x\exists y\left(A=⟨w,z⟩\wedge w=⟨x,y⟩\right)$$
4		19.42vv	$$⊢\exists x\exists y\left(A=⟨w,z⟩\wedge w=⟨x,y⟩\right)\leftrightarrow \left(A=⟨w,z⟩\wedge \exists x\exists yw=⟨x,y⟩\right)$$
5		elvv	$$⊢w\in \left(\mathrm{V}\times \mathrm{V}\right)\leftrightarrow \exists x\exists yw=⟨x,y⟩$$
6	5	anbi2i	$$⊢\left(A=⟨w,z⟩\wedge w\in \left(\mathrm{V}\times \mathrm{V}\right)\right)\leftrightarrow \left(A=⟨w,z⟩\wedge \exists x\exists yw=⟨x,y⟩\right)$$
7		vex	$$⊢z\in \mathrm{V}$$
8	7	biantru	$$⊢\left(A=⟨w,z⟩\wedge w\in \left(\mathrm{V}\times \mathrm{V}\right)\right)\leftrightarrow \left(\left(A=⟨w,z⟩\wedge w\in \left(\mathrm{V}\times \mathrm{V}\right)\right)\wedge z\in \mathrm{V}\right)$$
9	4 6 8	3bitr2i	$$⊢\exists x\exists y\left(A=⟨w,z⟩\wedge w=⟨x,y⟩\right)\leftrightarrow \left(\left(A=⟨w,z⟩\wedge w\in \left(\mathrm{V}\times \mathrm{V}\right)\right)\wedge z\in \mathrm{V}\right)$$
10		anass	$$⊢\left(\left(A=⟨w,z⟩\wedge w\in \left(\mathrm{V}\times \mathrm{V}\right)\right)\wedge z\in \mathrm{V}\right)\leftrightarrow \left(A=⟨w,z⟩\wedge \left(w\in \left(\mathrm{V}\times \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}\times \mathrm{V}\right)\wedge z\in \mathrm{V}\right)\right)\leftrightarrow \exists x\exists y\left(w=⟨x,y⟩\wedge A=⟨w,z⟩\right)$$
12	11	2exbii	$$⊢\exists w\exists z\left(A=⟨w,z⟩\wedge \left(w\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge z\in \mathrm{V}\right)\right)\leftrightarrow \exists w\exists z\exists x\exists y\left(w=⟨x,y⟩\wedge A=⟨w,z⟩\right)$$
13		exrot4	$$⊢\exists x\exists y\exists w\exists z\left(w=⟨x,y⟩\wedge A=⟨w,z⟩\right)\leftrightarrow \exists w\exists z\exists x\exists y\left(w=⟨x,y⟩\wedge A=⟨w,z⟩\right)$$
14		excom	$$⊢\exists w\exists z\left(w=⟨x,y⟩\wedge A=⟨w,z⟩\right)\leftrightarrow \exists z\exists w\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⟩\leftrightarrow A=⟨⟨x,y⟩,z⟩\right)$$
18	15 17	ceqsexv	$$⊢\exists w\left(w=⟨x,y⟩\wedge A=⟨w,z⟩\right)\leftrightarrow A=⟨⟨x,y⟩,z⟩$$
19	18	exbii	$$⊢\exists z\exists w\left(w=⟨x,y⟩\wedge A=⟨w,z⟩\right)\leftrightarrow \exists zA=⟨⟨x,y⟩,z⟩$$
20	14 19	bitri	$$⊢\exists w\exists z\left(w=⟨x,y⟩\wedge A=⟨w,z⟩\right)\leftrightarrow \exists zA=⟨⟨x,y⟩,z⟩$$
21	20	2exbii	$$⊢\exists x\exists y\exists w\exists z\left(w=⟨x,y⟩\wedge A=⟨w,z⟩\right)\leftrightarrow \exists x\exists y\exists zA=⟨⟨x,y⟩,z⟩$$
22	12 13 21	3bitr2i	$$⊢\exists w\exists z\left(A=⟨w,z⟩\wedge \left(w\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge z\in \mathrm{V}\right)\right)\leftrightarrow \exists x\exists y\exists zA=⟨⟨x,y⟩,z⟩$$
23	1 22	bitri	$$⊢A\in \left(\left(\mathrm{V}\times \mathrm{V}\right)\times \mathrm{V}\right)\leftrightarrow \exists x\exists y\exists zA=⟨⟨x,y⟩,z⟩$$