Theorem f0

Description: The empty function. (Contributed by NM, 14-Aug-1999)

	Ref	Expression
Assertion	f0	$$⊢\varnothing :\varnothing ⟶A$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\varnothing =\varnothing$$
2		fn0	$$⊢\varnothing Fn\varnothing \leftrightarrow \varnothing =\varnothing$$
3	1 2	mpbir	$$⊢\varnothing Fn\varnothing$$
4		rn0	$$⊢\mathrm{ran}\varnothing =\varnothing$$
5		0ss	$$⊢\varnothing \subseteq A$$
6	4 5	eqsstri	$$⊢\mathrm{ran}\varnothing \subseteq A$$
7		df-f	$$⊢\varnothing :\varnothing ⟶A\leftrightarrow \left(\varnothing Fn\varnothing \wedge \mathrm{ran}\varnothing \subseteq A\right)$$
8	3 6 7	mpbir2an	$$⊢\varnothing :\varnothing ⟶A$$