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

Metamath Proof Explorer

Theorem preq12b

Description: Equality relationship for two unordered pairs. (Contributed by NM, 17-Oct-1996)

Ref Expression
Hypotheses preqr1.a 
|- A e. _V
preqr1.b 
|- B e. _V
preq12b.c 
|- C e. _V
preq12b.d 
|- D e. _V
Assertion preq12b 
|- ( { A , B } = { C , D } <-> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) )

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 prid1 
 |-  A e. { A , B }
6 eleq2 
 |-  ( { A , B } = { C , D } -> ( A e. { A , B } <-> A e. { C , D } ) )
7 5 6 mpbii 
 |-  ( { A , B } = { C , D } -> A e. { C , D } )
8 1 elpr 
 |-  ( A e. { C , D } <-> ( A = C \/ A = D ) )
9 7 8 sylib 
 |-  ( { A , B } = { C , D } -> ( A = C \/ A = D ) )
10 preq1 
 |-  ( A = C -> { A , B } = { C , B } )
11 10 eqeq1d 
 |-  ( A = C -> ( { A , B } = { C , D } <-> { C , B } = { C , D } ) )
12 2 4 preqr2 
 |-  ( { C , B } = { C , D } -> B = D )
13 11 12 biimtrdi 
 |-  ( A = C -> ( { A , B } = { C , D } -> B = D ) )
14 13 com12 
 |-  ( { A , B } = { C , D } -> ( A = C -> B = D ) )
15 14 ancld 
 |-  ( { A , B } = { C , D } -> ( A = C -> ( A = C /\ B = D ) ) )
16 prcom 
 |-  { C , D } = { D , C }
17 16 eqeq2i 
 |-  ( { A , B } = { C , D } <-> { A , B } = { D , C } )
18 preq1 
 |-  ( A = D -> { A , B } = { D , B } )
19 18 eqeq1d 
 |-  ( A = D -> ( { A , B } = { D , C } <-> { D , B } = { D , C } ) )
20 2 3 preqr2 
 |-  ( { D , B } = { D , C } -> B = C )
21 19 20 biimtrdi 
 |-  ( A = D -> ( { A , B } = { D , C } -> B = C ) )
22 21 com12 
 |-  ( { A , B } = { D , C } -> ( A = D -> B = C ) )
23 17 22 sylbi 
 |-  ( { A , B } = { C , D } -> ( A = D -> B = C ) )
24 23 ancld 
 |-  ( { A , B } = { C , D } -> ( A = D -> ( A = D /\ B = C ) ) )
25 15 24 orim12d 
 |-  ( { A , B } = { C , D } -> ( ( A = C \/ A = D ) -> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) ) )
26 9 25 mpd 
 |-  ( { A , B } = { C , D } -> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) )
27 preq12 
 |-  ( ( A = C /\ B = D ) -> { A , B } = { C , D } )
28 preq12 
 |-  ( ( A = D /\ B = C ) -> { A , B } = { D , C } )
29 prcom 
 |-  { D , C } = { C , D }
30 28 29 eqtrdi 
 |-  ( ( A = D /\ B = C ) -> { A , B } = { C , D } )
31 27 30 jaoi 
 |-  ( ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) -> { A , B } = { C , D } )
32 26 31 impbii 
 |-  ( { A , B } = { C , D } <-> ( ( A = C /\ B = D ) \/ ( A = D /\ B = C ) ) )