opthpr

Description: An unordered pair has the ordered pair property (compare opth ) under certain conditions. (Contributed by NM, 27-Mar-2007)

	Ref	Expression
Hypotheses	preqr1.a	$⊢ A \in V$
	preqr1.b	$⊢ B \in V$
	preq12b.c	$⊢ C \in V$
	preq12b.d	$⊢ D \in V$
Assertion	opthpr	$⊢ A \neq D \to (\{A, B\} = \{C, D\} \leftrightarrow (A = C \land B = D))$

Step	Hyp	Ref	Expression
1		preqr1.a	$⊢ A \in V$
2		preqr1.b	$⊢ B \in V$
3		preq12b.c	$⊢ C \in V$
4		preq12b.d	$⊢ D \in V$
5	1 2 3 4	preq12b	$⊢ \{A, B\} = \{C, D\} \leftrightarrow ((A = C \land B = D) \lor (A = D \land B = C))$
6		idd	$⊢ A \neq D \to ((A = C \land B = D) \to (A = C \land B = D))$
7		df-ne	$⊢ A \neq D \leftrightarrow \neg A = D$
8		pm2.21	$⊢ \neg A = D \to (A = D \to (B = C \to (A = C \land B = D)))$
9	7 8	sylbi	$⊢ A \neq D \to (A = D \to (B = C \to (A = C \land B = D)))$
10	9	impd	$⊢ A \neq D \to ((A = D \land B = C) \to (A = C \land B = D))$
11	6 10	jaod	$⊢ A \neq D \to (((A = C \land B = D) \lor (A = D \land B = C)) \to (A = C \land B = D))$
12		orc	$⊢ (A = C \land B = D) \to ((A = C \land B = D) \lor (A = D \land B = C))$
13	11 12	impbid1	$⊢ A \neq D \to (((A = C \land B = D) \lor (A = D \land B = C)) \leftrightarrow (A = C \land B = D))$
14	5 13	bitrid	$⊢ A \neq D \to (\{A, B\} = \{C, D\} \leftrightarrow (A = C \land B = D))$

Metamath Proof Explorer