elxp2

Description: Membership in a Cartesian product. (Contributed by NM, 23-Feb-2004) (Proof shortened by JJ, 13-Aug-2021)

		Ref	Expression
	Assertion	elxp2	$⊢ A \in (B \times C) \leftrightarrow \exists x \in B \exists y \in C A = ⟨x, y⟩$

Step	Hyp	Ref	Expression
1		ancom	$⊢ (A = ⟨x, y⟩ \land (x \in B \land y \in C)) \leftrightarrow ((x \in B \land y \in C) \land A = ⟨x, y⟩)$
2	1	2exbii	$⊢ \exists x \exists y (A = ⟨x, y⟩ \land (x \in B \land y \in C)) \leftrightarrow \exists x \exists y ((x \in B \land y \in C) \land A = ⟨x, y⟩)$
3		elxp	$⊢ A \in (B \times C) \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land (x \in B \land y \in C))$
4		r2ex	$⊢ \exists x \in B \exists y \in C A = ⟨x, y⟩ \leftrightarrow \exists x \exists y ((x \in B \land y \in C) \land A = ⟨x, y⟩)$
5	2 3 4	3bitr4i	$⊢ A \in (B \times C) \leftrightarrow \exists x \in B \exists y \in C A = ⟨x, y⟩$

Metamath Proof Explorer