Theorem 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	⊢ 𝐴 ∈ V
	preqr1.b	⊢ 𝐵 ∈ V
	preq12b.c	⊢ 𝐶 ∈ V
	preq12b.d	⊢ 𝐷 ∈ V
Assertion	opthpr	⊢ ( 𝐴 ≠ 𝐷 → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		preqr1.a	⊢ 𝐴 ∈ V
2		preqr1.b	⊢ 𝐵 ∈ V
3		preq12b.c	⊢ 𝐶 ∈ V
4		preq12b.d	⊢ 𝐷 ∈ V
5	1 2 3 4	preq12b	⊢ ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ↔ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) )
6		idd	⊢ ( 𝐴 ≠ 𝐷 → ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
7		df-ne	⊢ ( 𝐴 ≠ 𝐷 ↔ ¬ 𝐴 = 𝐷 )
8		pm2.21	⊢ ( ¬ 𝐴 = 𝐷 → ( 𝐴 = 𝐷 → ( 𝐵 = 𝐶 → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) ) )
9	7 8	sylbi	⊢ ( 𝐴 ≠ 𝐷 → ( 𝐴 = 𝐷 → ( 𝐵 = 𝐶 → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) ) )
10	9	impd	⊢ ( 𝐴 ≠ 𝐷 → ( ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
11	6 10	jaod	⊢ ( 𝐴 ≠ 𝐷 → ( ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
12		orc	⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) )
13	11 12	impbid1	⊢ ( 𝐴 ≠ 𝐷 → ( ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
14	5 13	bitrid	⊢ ( 𝐴 ≠ 𝐷 → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )