Metamath Proof Explorer


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 syl5bb
 |-  ( A =/= D -> ( { A , B } = { C , D } <-> ( A = C /\ B = D ) ) )