Metamath Proof Explorer


Theorem f00

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 F:AF=A=

Proof

Step Hyp Ref Expression
1 ffun F:AFunF
2 frn F:AranF
3 ss0 ranFranF=
4 2 3 syl F:AranF=
5 dm0rn0 domF=ranF=
6 4 5 sylibr F:AdomF=
7 df-fn FFnFunFdomF=
8 1 6 7 sylanbrc F:AFFn
9 fn0 FFnF=
10 8 9 sylib F:AF=
11 fdm F:AdomF=A
12 11 6 eqtr3d F:AA=
13 10 12 jca F:AF=A=
14 f0 :
15 feq1 F=F:A:A
16 feq2 A=:A:
17 15 16 sylan9bb F=A=F:A:
18 14 17 mpbiri F=A=F:A
19 13 18 impbii F:AF=A=