This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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