Theorem fun0

Description: The empty set is a function. Theorem 10.3 of Quine p. 65. (Contributed by NM, 7-Apr-1998)

	Ref	Expression
Assertion	fun0	$$⊢\mathrm{Fun}\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		0ss	$$⊢\varnothing \subseteq \left\{⟨\varnothing ,\varnothing ⟩\right\}$$
2		0ex	$$⊢\varnothing \in \mathrm{V}$$
3	2 2	funsn	$$⊢\mathrm{Fun}\left\{⟨\varnothing ,\varnothing ⟩\right\}$$
4		funss	$$⊢\varnothing \subseteq \left\{⟨\varnothing ,\varnothing ⟩\right\}\to \left(\mathrm{Fun}\left\{⟨\varnothing ,\varnothing ⟩\right\}\to \mathrm{Fun}\varnothing \right)$$
5	1 3 4	mp2	$$⊢\mathrm{Fun}\varnothing$$