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