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	|- A e. _V
	preqr1.b	|- B e. _V
	preq12b.c	|- C e. _V
	preq12b.d	|- D e. _V
Assertion	opthpr	|- ( A =/= D -> ( { A , B } = { C , D } <-> ( A = C /\ B = D ) ) )

Proof

Step	Hyp	Ref	Expression
1		preqr1.a	|- A e. _V
2		preqr1.b	|- B e. _V
3		preq12b.c	|- C e. _V
4		preq12b.d	|- D e. _V
5	1 2 3 4	preq12b	|- ( { A , B } = { C , D } <-> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) )
6		idd	|- ( A =/= D -> ( ( A = C /\ B = D ) -> ( A = C /\ B = D ) ) )
7		df-ne	|- ( A =/= D <-> -. A = D )
8		pm2.21	|- ( -. A = D -> ( A = D -> ( B = C -> ( A = C /\ B = D ) ) ) )
9	7 8	sylbi	|- ( A =/= D -> ( A = D -> ( B = C -> ( A = C /\ B = D ) ) ) )
10	9	impd	|- ( A =/= D -> ( ( A = D /\ B = C ) -> ( A = C /\ B = D ) ) )
11	6 10	jaod	|- ( A =/= D -> ( ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) -> ( A = C /\ B = D ) ) )
12		orc	|- ( ( A = C /\ B = D ) -> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) )
13	11 12	impbid1	|- ( A =/= D -> ( ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) <-> ( A = C /\ B = D ) ) )
14	5 13	bitrid	|- ( A =/= D -> ( { A , B } = { C , D } <-> ( A = C /\ B = D ) ) )