Description: A class is a function with empty codomain iff it and its domain are empty. (Contributed by NM, 10-Dec-2003)
Ref | Expression | ||
---|---|---|---|
Assertion | f00 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ffun | |
|
2 | frn | |
|
3 | ss0 | |
|
4 | 2 3 | syl | |
5 | dm0rn0 | |
|
6 | 4 5 | sylibr | |
7 | df-fn | |
|
8 | 1 6 7 | sylanbrc | |
9 | fn0 | |
|
10 | 8 9 | sylib | |
11 | fdm | |
|
12 | 11 6 | eqtr3d | |
13 | 10 12 | jca | |
14 | f0 | |
|
15 | feq1 | |
|
16 | feq2 | |
|
17 | 15 16 | sylan9bb | |
18 | 14 17 | mpbiri | |
19 | 13 18 | impbii | |