# Metamath Proof Explorer

## Theorem fn0

Description: A function with empty domain is empty. (Contributed by NM, 15-Apr-1998) (Proof shortened by Andrew Salmon, 17-Sep-2011)

Ref Expression
Assertion fn0 ${⊢}{F}Fn\varnothing ↔{F}=\varnothing$

### Proof

Step Hyp Ref Expression
1 fnrel ${⊢}{F}Fn\varnothing \to \mathrm{Rel}{F}$
2 fndm ${⊢}{F}Fn\varnothing \to \mathrm{dom}{F}=\varnothing$
3 reldm0 ${⊢}\mathrm{Rel}{F}\to \left({F}=\varnothing ↔\mathrm{dom}{F}=\varnothing \right)$
4 3 biimpar ${⊢}\left(\mathrm{Rel}{F}\wedge \mathrm{dom}{F}=\varnothing \right)\to {F}=\varnothing$
5 1 2 4 syl2anc ${⊢}{F}Fn\varnothing \to {F}=\varnothing$
6 fun0 ${⊢}\mathrm{Fun}\varnothing$
7 dm0 ${⊢}\mathrm{dom}\varnothing =\varnothing$
8 df-fn ${⊢}\varnothing Fn\varnothing ↔\left(\mathrm{Fun}\varnothing \wedge \mathrm{dom}\varnothing =\varnothing \right)$
9 6 7 8 mpbir2an ${⊢}\varnothing Fn\varnothing$
10 fneq1 ${⊢}{F}=\varnothing \to \left({F}Fn\varnothing ↔\varnothing Fn\varnothing \right)$
11 9 10 mpbiri ${⊢}{F}=\varnothing \to {F}Fn\varnothing$
12 5 11 impbii ${⊢}{F}Fn\varnothing ↔{F}=\varnothing$