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 = w \to (z = ⟨x, y⟩ \leftrightarrow w = ⟨x, y⟩)$
2	1	anbi1d	$⊢ z = w \to ((z = ⟨x, y⟩ \land (x \in B \land y \in C)) \leftrightarrow (w = ⟨x, y⟩ \land (x \in B \land y \in C)))$
3	2	2exbidv	$⊢ z = w \to (\exists x \exists y (z = ⟨x, y⟩ \land (x \in B \land y \in C)) \leftrightarrow \exists x \exists y (w = ⟨x, y⟩ \land (x \in B \land y \in C)))$
4		eqeq1	$⊢ w = A \to (w = ⟨x, y⟩ \leftrightarrow A = ⟨x, y⟩)$
5	4	anbi1d	$⊢ w = A \to ((w = ⟨x, y⟩ \land (x \in B \land y \in C)) \leftrightarrow (A = ⟨x, y⟩ \land (x \in B \land y \in C)))$
6	5	2exbidv	$⊢ w = A \to (\exists x \exists y (w = ⟨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)))$
7		df-xp	$⊢ B \times C = \{⟨x, y⟩ \| (x \in B \land y \in C)\}$
8		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))\}$
9	7 8	eqtri	$⊢ B \times C = \{z \| \exists x \exists y (z = ⟨x, y⟩ \land (x \in B \land y \in C))\}$
10	3 6 9	elab2gw	$⊢ 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)))$
11	10	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