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 ∅

Proof

Step Hyp Ref Expression
1 0ss ∅ ⊆ { ⟨ ∅ , ∅ ⟩ }
2 0ex ∅ ∈ V
3 2 2 funsn Fun { ⟨ ∅ , ∅ ⟩ }
4 funss ( ∅ ⊆ { ⟨ ∅ , ∅ ⟩ } → ( Fun { ⟨ ∅ , ∅ ⟩ } → Fun ∅ ) )
5 1 3 4 mp2 Fun ∅