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