elxpi

Description: Membership in a Cartesian product. Uses fewer axioms than elxp . (Contributed by NM, 4-Jul-1994)

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

Step	Hyp	Ref	Expression
1		eqeq1	$⊢ z = A \to (z = ⟨x, y⟩ \leftrightarrow A = ⟨x, y⟩)$
2	1	anbi1d	$⊢ z = A \to ((z = ⟨x, y⟩ \land (x \in B \land y \in C)) \leftrightarrow (A = ⟨x, y⟩ \land (x \in B \land y \in C)))$
3	2	2exbidv	$⊢ z = A \to (\exists x \exists y (z = ⟨x, y⟩ \land (x \in B \land y \in C)) \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land (x \in B \land y \in C)))$
4		df-xp	$⊢ B \times C = \{⟨x, y⟩ \| (x \in B \land y \in C)\}$
5		df-opab	$⊢ \{⟨x, y⟩ \| (x \in B \land y \in C)\} = \{z \| \exists x \exists y (z = ⟨x, y⟩ \land (x \in B \land y \in C))\}$
6	4 5	eqtri	$⊢ B \times C = \{z \| \exists x \exists y (z = ⟨x, y⟩ \land (x \in B \land y \in C))\}$
7	3 6	elab2g	$⊢ A \in (B \times C) \to (A \in (B \times C) \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land (x \in B \land y \in C)))$
8	7	ibi	$⊢ A \in (B \times C) \to \exists x \exists y (A = ⟨x, y⟩ \land (x \in B \land y \in C))$

Metamath Proof Explorer