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 syl6bi
 |-  ( 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 syl6bi
 |-  ( 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 ) ) )