Metamath Proof Explorer

Theorem opelxp

Description: Ordered pair membership in a Cartesian product. (Contributed by NM, 15-Nov-1994) (Proof shortened by Andrew Salmon, 12-Aug-2011) (Revised by Mario Carneiro, 26-Apr-2015)

		Ref	Expression
	Assertion	opelxp	$⊢ ⟨A, B⟩ \in (C \times D) \leftrightarrow (A \in C \land B \in D)$

Proof

Step	Hyp	Ref	Expression
1		elxp2	$⊢ ⟨A, B⟩ \in (C \times D) \leftrightarrow \exists x \in C \exists y \in D ⟨A, B⟩ = ⟨x, y⟩$
2		vex	$⊢ x \in V$
3		vex	$⊢ y \in V$
4	2 3	opth2	$⊢ ⟨A, B⟩ = ⟨x, y⟩ \leftrightarrow (A = x \land B = y)$
5		eleq1	$⊢ A = x \to (A \in C \leftrightarrow x \in C)$
6		eleq1	$⊢ B = y \to (B \in D \leftrightarrow y \in D)$
7	5 6	bi2anan9	$⊢ (A = x \land B = y) \to ((A \in C \land B \in D) \leftrightarrow (x \in C \land y \in D))$
8	4 7	sylbi	$⊢ ⟨A, B⟩ = ⟨x, y⟩ \to ((A \in C \land B \in D) \leftrightarrow (x \in C \land y \in D))$
9	8	biimprcd	$⊢ (x \in C \land y \in D) \to (⟨A, B⟩ = ⟨x, y⟩ \to (A \in C \land B \in D))$
10	9	rexlimivv	$⊢ \exists x \in C \exists y \in D ⟨A, B⟩ = ⟨x, y⟩ \to (A \in C \land B \in D)$
11		eqid	$⊢ ⟨A, B⟩ = ⟨A, B⟩$
12		opeq1	$⊢ x = A \to ⟨x, y⟩ = ⟨A, y⟩$
13	12	eqeq2d	$⊢ x = A \to (⟨A, B⟩ = ⟨x, y⟩ \leftrightarrow ⟨A, B⟩ = ⟨A, y⟩)$
14		opeq2	$⊢ y = B \to ⟨A, y⟩ = ⟨A, B⟩$
15	14	eqeq2d	$⊢ y = B \to (⟨A, B⟩ = ⟨A, y⟩ \leftrightarrow ⟨A, B⟩ = ⟨A, B⟩)$
16	13 15	rspc2ev	$⊢ (A \in C \land B \in D \land ⟨A, B⟩ = ⟨A, B⟩) \to \exists x \in C \exists y \in D ⟨A, B⟩ = ⟨x, y⟩$
17	11 16	mp3an3	$⊢ (A \in C \land B \in D) \to \exists x \in C \exists y \in D ⟨A, B⟩ = ⟨x, y⟩$
18	10 17	impbii	$⊢ \exists x \in C \exists y \in D ⟨A, B⟩ = ⟨x, y⟩ \leftrightarrow (A \in C \land B \in D)$
19	1 18	bitri	$⊢ ⟨A, B⟩ \in (C \times D) \leftrightarrow (A \in C \land B \in D)$