This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ Fun \emptyset$

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