| Step |
Hyp |
Ref |
Expression |
| 1 |
|
eupth2lem2.1 |
|- B e. _V |
| 2 |
|
eqidd |
|- ( ( B =/= C /\ B = U ) -> B = B ) |
| 3 |
2
|
olcd |
|- ( ( B =/= C /\ B = U ) -> ( B = A \/ B = B ) ) |
| 4 |
3
|
biantrud |
|- ( ( B =/= C /\ B = U ) -> ( A =/= B <-> ( A =/= B /\ ( B = A \/ B = B ) ) ) ) |
| 5 |
|
eupth2lem1 |
|- ( B e. _V -> ( B e. if ( A = B , (/) , { A , B } ) <-> ( A =/= B /\ ( B = A \/ B = B ) ) ) ) |
| 6 |
1 5
|
ax-mp |
|- ( B e. if ( A = B , (/) , { A , B } ) <-> ( A =/= B /\ ( B = A \/ B = B ) ) ) |
| 7 |
4 6
|
bitr4di |
|- ( ( B =/= C /\ B = U ) -> ( A =/= B <-> B e. if ( A = B , (/) , { A , B } ) ) ) |
| 8 |
|
simpr |
|- ( ( B =/= C /\ B = U ) -> B = U ) |
| 9 |
8
|
eleq1d |
|- ( ( B =/= C /\ B = U ) -> ( B e. if ( A = B , (/) , { A , B } ) <-> U e. if ( A = B , (/) , { A , B } ) ) ) |
| 10 |
7 9
|
bitrd |
|- ( ( B =/= C /\ B = U ) -> ( A =/= B <-> U e. if ( A = B , (/) , { A , B } ) ) ) |
| 11 |
10
|
necon1bbid |
|- ( ( B =/= C /\ B = U ) -> ( -. U e. if ( A = B , (/) , { A , B } ) <-> A = B ) ) |
| 12 |
|
simpl |
|- ( ( B =/= C /\ B = U ) -> B =/= C ) |
| 13 |
|
neeq1 |
|- ( B = A -> ( B =/= C <-> A =/= C ) ) |
| 14 |
12 13
|
syl5ibcom |
|- ( ( B =/= C /\ B = U ) -> ( B = A -> A =/= C ) ) |
| 15 |
14
|
pm4.71rd |
|- ( ( B =/= C /\ B = U ) -> ( B = A <-> ( A =/= C /\ B = A ) ) ) |
| 16 |
|
eqcom |
|- ( A = B <-> B = A ) |
| 17 |
|
ancom |
|- ( ( B = A /\ A =/= C ) <-> ( A =/= C /\ B = A ) ) |
| 18 |
15 16 17
|
3bitr4g |
|- ( ( B =/= C /\ B = U ) -> ( A = B <-> ( B = A /\ A =/= C ) ) ) |
| 19 |
12
|
neneqd |
|- ( ( B =/= C /\ B = U ) -> -. B = C ) |
| 20 |
|
biorf |
|- ( -. B = C -> ( B = A <-> ( B = C \/ B = A ) ) ) |
| 21 |
19 20
|
syl |
|- ( ( B =/= C /\ B = U ) -> ( B = A <-> ( B = C \/ B = A ) ) ) |
| 22 |
|
orcom |
|- ( ( B = C \/ B = A ) <-> ( B = A \/ B = C ) ) |
| 23 |
21 22
|
bitrdi |
|- ( ( B =/= C /\ B = U ) -> ( B = A <-> ( B = A \/ B = C ) ) ) |
| 24 |
23
|
anbi1d |
|- ( ( B =/= C /\ B = U ) -> ( ( B = A /\ A =/= C ) <-> ( ( B = A \/ B = C ) /\ A =/= C ) ) ) |
| 25 |
18 24
|
bitrd |
|- ( ( B =/= C /\ B = U ) -> ( A = B <-> ( ( B = A \/ B = C ) /\ A =/= C ) ) ) |
| 26 |
|
ancom |
|- ( ( A =/= C /\ ( B = A \/ B = C ) ) <-> ( ( B = A \/ B = C ) /\ A =/= C ) ) |
| 27 |
25 26
|
bitr4di |
|- ( ( B =/= C /\ B = U ) -> ( A = B <-> ( A =/= C /\ ( B = A \/ B = C ) ) ) ) |
| 28 |
|
eupth2lem1 |
|- ( B e. _V -> ( B e. if ( A = C , (/) , { A , C } ) <-> ( A =/= C /\ ( B = A \/ B = C ) ) ) ) |
| 29 |
1 28
|
ax-mp |
|- ( B e. if ( A = C , (/) , { A , C } ) <-> ( A =/= C /\ ( B = A \/ B = C ) ) ) |
| 30 |
8
|
eleq1d |
|- ( ( B =/= C /\ B = U ) -> ( B e. if ( A = C , (/) , { A , C } ) <-> U e. if ( A = C , (/) , { A , C } ) ) ) |
| 31 |
29 30
|
bitr3id |
|- ( ( B =/= C /\ B = U ) -> ( ( A =/= C /\ ( B = A \/ B = C ) ) <-> U e. if ( A = C , (/) , { A , C } ) ) ) |
| 32 |
11 27 31
|
3bitrd |
|- ( ( B =/= C /\ B = U ) -> ( -. U e. if ( A = B , (/) , { A , B } ) <-> U e. if ( A = C , (/) , { A , C } ) ) ) |