| Step |
Hyp |
Ref |
Expression |
| 1 |
|
encv |
|- ( (/) ~~ A -> ( (/) e. _V /\ A e. _V ) ) |
| 2 |
|
breng |
|- ( ( (/) e. _V /\ A e. _V ) -> ( (/) ~~ A <-> E. f f : (/) -1-1-onto-> A ) ) |
| 3 |
1 2
|
syl |
|- ( (/) ~~ A -> ( (/) ~~ A <-> E. f f : (/) -1-1-onto-> A ) ) |
| 4 |
3
|
ibi |
|- ( (/) ~~ A -> E. f f : (/) -1-1-onto-> A ) |
| 5 |
|
f1o00 |
|- ( f : (/) -1-1-onto-> A <-> ( f = (/) /\ A = (/) ) ) |
| 6 |
5
|
simprbi |
|- ( f : (/) -1-1-onto-> A -> A = (/) ) |
| 7 |
6
|
exlimiv |
|- ( E. f f : (/) -1-1-onto-> A -> A = (/) ) |
| 8 |
4 7
|
syl |
|- ( (/) ~~ A -> A = (/) ) |
| 9 |
|
0ex |
|- (/) e. _V |
| 10 |
|
f1oeq1 |
|- ( f = (/) -> ( f : (/) -1-1-onto-> (/) <-> (/) : (/) -1-1-onto-> (/) ) ) |
| 11 |
|
f1o0 |
|- (/) : (/) -1-1-onto-> (/) |
| 12 |
9 10 11
|
ceqsexv2d |
|- E. f f : (/) -1-1-onto-> (/) |
| 13 |
|
breng |
|- ( ( (/) e. _V /\ (/) e. _V ) -> ( (/) ~~ (/) <-> E. f f : (/) -1-1-onto-> (/) ) ) |
| 14 |
9 9 13
|
mp2an |
|- ( (/) ~~ (/) <-> E. f f : (/) -1-1-onto-> (/) ) |
| 15 |
12 14
|
mpbir |
|- (/) ~~ (/) |
| 16 |
|
breq2 |
|- ( A = (/) -> ( (/) ~~ A <-> (/) ~~ (/) ) ) |
| 17 |
15 16
|
mpbiri |
|- ( A = (/) -> (/) ~~ A ) |
| 18 |
8 17
|
impbii |
|- ( (/) ~~ A <-> A = (/) ) |