Theorem el2xptp

Description: A member of a nested Cartesian product is an ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018)

	Ref	Expression
Assertion	el2xptp	$$⊢A\in \left(\left(B\times C\right)\times D\right)\leftrightarrow \exists x\in B\exists y\in C\exists z\in DA=⟨x,y,z⟩$$

Proof

Step	Hyp	Ref	Expression
1		elxp2	$$⊢A\in \left(\left(B\times C\right)\times D\right)\leftrightarrow \exists p\in \left(B\times C\right)\exists z\in DA=⟨p,z⟩$$
2		opeq1	$$⊢p=⟨x,y⟩\to ⟨p,z⟩=⟨⟨x,y⟩,z⟩$$
3	2	eqeq2d	$$⊢p=⟨x,y⟩\to \left(A=⟨p,z⟩\leftrightarrow A=⟨⟨x,y⟩,z⟩\right)$$
4	3	rexbidv	$$⊢p=⟨x,y⟩\to \left(\exists z\in DA=⟨p,z⟩\leftrightarrow \exists z\in DA=⟨⟨x,y⟩,z⟩\right)$$
5	4	rexxp	$$⊢\exists p\in \left(B\times C\right)\exists z\in DA=⟨p,z⟩\leftrightarrow \exists x\in B\exists y\in C\exists z\in DA=⟨⟨x,y⟩,z⟩$$
6		df-ot	$$⊢⟨x,y,z⟩=⟨⟨x,y⟩,z⟩$$
7	6	eqcomi	$$⊢⟨⟨x,y⟩,z⟩=⟨x,y,z⟩$$
8	7	eqeq2i	$$⊢A=⟨⟨x,y⟩,z⟩\leftrightarrow A=⟨x,y,z⟩$$
9	8	rexbii	$$⊢\exists z\in DA=⟨⟨x,y⟩,z⟩\leftrightarrow \exists z\in DA=⟨x,y,z⟩$$
10	9	rexbii	$$⊢\exists y\in C\exists z\in DA=⟨⟨x,y⟩,z⟩\leftrightarrow \exists y\in C\exists z\in DA=⟨x,y,z⟩$$
11	10	rexbii	$$⊢\exists x\in B\exists y\in C\exists z\in DA=⟨⟨x,y⟩,z⟩\leftrightarrow \exists x\in B\exists y\in C\exists z\in DA=⟨x,y,z⟩$$
12	1 5 11	3bitri	$$⊢A\in \left(\left(B\times C\right)\times D\right)\leftrightarrow \exists x\in B\exists y\in C\exists z\in DA=⟨x,y,z⟩$$