Metamath Proof Explorer

Theorem opthg

Description: Ordered pair theorem. C and D are not required to be sets under our specific ordered pair definition. (Contributed by NM, 14-Oct-2005) (Revised by Mario Carneiro, 26-Apr-2015)

		Ref	Expression
	Assertion	opthg	$⊢ (A \in V \land B \in W) \to (⟨A, B⟩ = ⟨C, D⟩ \leftrightarrow (A = C \land B = D))$

Proof

Step	Hyp	Ref	Expression
1		opeq1	$⊢ x = A \to ⟨x, y⟩ = ⟨A, y⟩$
2	1	eqeq1d	$⊢ x = A \to (⟨x, y⟩ = ⟨C, D⟩ \leftrightarrow ⟨A, y⟩ = ⟨C, D⟩)$
3		eqeq1	$⊢ x = A \to (x = C \leftrightarrow A = C)$
4	3	anbi1d	$⊢ x = A \to ((x = C \land y = D) \leftrightarrow (A = C \land y = D))$
5	2 4	bibi12d	$⊢ x = A \to ((⟨x, y⟩ = ⟨C, D⟩ \leftrightarrow (x = C \land y = D)) \leftrightarrow (⟨A, y⟩ = ⟨C, D⟩ \leftrightarrow (A = C \land y = D)))$
6		opeq2	$⊢ y = B \to ⟨A, y⟩ = ⟨A, B⟩$
7	6	eqeq1d	$⊢ y = B \to (⟨A, y⟩ = ⟨C, D⟩ \leftrightarrow ⟨A, B⟩ = ⟨C, D⟩)$
8		eqeq1	$⊢ y = B \to (y = D \leftrightarrow B = D)$
9	8	anbi2d	$⊢ y = B \to ((A = C \land y = D) \leftrightarrow (A = C \land B = D))$
10	7 9	bibi12d	$⊢ y = B \to ((⟨A, y⟩ = ⟨C, D⟩ \leftrightarrow (A = C \land y = D)) \leftrightarrow (⟨A, B⟩ = ⟨C, D⟩ \leftrightarrow (A = C \land B = D)))$
11		vex	$⊢ x \in V$
12		vex	$⊢ y \in V$
13	11 12	opth	$⊢ ⟨x, y⟩ = ⟨C, D⟩ \leftrightarrow (x = C \land y = D)$
14	5 10 13	vtocl2g	$⊢ (A \in V \land B \in W) \to (⟨A, B⟩ = ⟨C, D⟩ \leftrightarrow (A = C \land B = D))$