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 
 |-  (/) C_ { <. (/) , (/) >. }
2 0ex 
 |-  (/) e. _V
3 2 2 funsn 
 |-  Fun { <. (/) , (/) >. }
4 funss 
 |-  ( (/) C_ { <. (/) , (/) >. } -> ( Fun { <. (/) , (/) >. } -> Fun (/) ) )
5 1 3 4 mp2 
 |-  Fun (/)