elxp3

Description: Membership in a Cartesian product. (Contributed by NM, 5-Mar-1995)

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

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

Metamath Proof Explorer