Theorem elxpxp

Description: Membership in a triple cross product. (Contributed by Scott Fenton, 21-Aug-2024)

	Ref	Expression
Assertion	elxpxp	$$⊢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	1 5	bitri	$$⊢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⟩$$