elvvv

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

		Ref	Expression
	Assertion	elvvv	$⊢ A \in ((V \times V) \times V) \leftrightarrow \exists x \exists y \exists z A = ⟨⟨x, y⟩, z⟩$

Proof

Step	Hyp	Ref	Expression
1		elxp	$⊢ A \in ((V \times V) \times V) \leftrightarrow \exists w \exists z (A = ⟨w, z⟩ \land (w \in (V \times V) \land z \in V))$
2		ancom	$⊢ (w = ⟨x, y⟩ \land A = ⟨w, z⟩) \leftrightarrow (A = ⟨w, z⟩ \land w = ⟨x, y⟩)$
3	2	2exbii	$⊢ \exists x \exists y (w = ⟨x, y⟩ \land A = ⟨w, z⟩) \leftrightarrow \exists x \exists y (A = ⟨w, z⟩ \land w = ⟨x, y⟩)$
4		19.42vv	$⊢ \exists x \exists y (A = ⟨w, z⟩ \land w = ⟨x, y⟩) \leftrightarrow (A = ⟨w, z⟩ \land \exists x \exists y w = ⟨x, y⟩)$
5		elvv	$⊢ w \in (V \times V) \leftrightarrow \exists x \exists y w = ⟨x, y⟩$
6	5	anbi2i	$⊢ (A = ⟨w, z⟩ \land w \in (V \times V)) \leftrightarrow (A = ⟨w, z⟩ \land \exists x \exists y w = ⟨x, y⟩)$
7		vex	$⊢ z \in V$
8	7	biantru	$⊢ (A = ⟨w, z⟩ \land w \in (V \times V)) \leftrightarrow ((A = ⟨w, z⟩ \land w \in (V \times V)) \land z \in V)$
9	4 6 8	3bitr2i	$⊢ \exists x \exists y (A = ⟨w, z⟩ \land w = ⟨x, y⟩) \leftrightarrow ((A = ⟨w, z⟩ \land w \in (V \times V)) \land z \in V)$
10		anass	$⊢ ((A = ⟨w, z⟩ \land w \in (V \times V)) \land z \in V) \leftrightarrow (A = ⟨w, z⟩ \land (w \in (V \times V) \land z \in V))$
11	3 9 10	3bitrri	$⊢ (A = ⟨w, z⟩ \land (w \in (V \times V) \land z \in V)) \leftrightarrow \exists x \exists y (w = ⟨x, y⟩ \land A = ⟨w, z⟩)$
12	11	2exbii	$⊢ \exists w \exists z (A = ⟨w, z⟩ \land (w \in (V \times V) \land z \in V)) \leftrightarrow \exists w \exists z \exists x \exists y (w = ⟨x, y⟩ \land A = ⟨w, z⟩)$
13		exrot4	$⊢ \exists x \exists y \exists w \exists z (w = ⟨x, y⟩ \land A = ⟨w, z⟩) \leftrightarrow \exists w \exists z \exists x \exists y (w = ⟨x, y⟩ \land A = ⟨w, z⟩)$
14		excom	$⊢ \exists w \exists z (w = ⟨x, y⟩ \land A = ⟨w, z⟩) \leftrightarrow \exists z \exists w (w = ⟨x, y⟩ \land A = ⟨w, z⟩)$
15		opex	$⊢ ⟨x, y⟩ \in V$
16		opeq1	$⊢ w = ⟨x, y⟩ \to ⟨w, z⟩ = ⟨⟨x, y⟩, z⟩$
17	16	eqeq2d	$⊢ w = ⟨x, y⟩ \to (A = ⟨w, z⟩ \leftrightarrow A = ⟨⟨x, y⟩, z⟩)$
18	15 17	ceqsexv	$⊢ \exists w (w = ⟨x, y⟩ \land A = ⟨w, z⟩) \leftrightarrow A = ⟨⟨x, y⟩, z⟩$
19	18	exbii	$⊢ \exists z \exists w (w = ⟨x, y⟩ \land A = ⟨w, z⟩) \leftrightarrow \exists z A = ⟨⟨x, y⟩, z⟩$
20	14 19	bitri	$⊢ \exists w \exists z (w = ⟨x, y⟩ \land A = ⟨w, z⟩) \leftrightarrow \exists z A = ⟨⟨x, y⟩, z⟩$
21	20	2exbii	$⊢ \exists x \exists y \exists w \exists z (w = ⟨x, y⟩ \land A = ⟨w, z⟩) \leftrightarrow \exists x \exists y \exists z A = ⟨⟨x, y⟩, z⟩$
22	12 13 21	3bitr2i	$⊢ \exists w \exists z (A = ⟨w, z⟩ \land (w \in (V \times V) \land z \in V)) \leftrightarrow \exists x \exists y \exists z A = ⟨⟨x, y⟩, z⟩$
23	1 22	bitri	$⊢ A \in ((V \times V) \times V) \leftrightarrow \exists x \exists y \exists z A = ⟨⟨x, y⟩, z⟩$

Metamath Proof Explorer

Theorem elvvv

Proof