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	⊢ ( 𝐹 Fn ∅ ↔ 𝐹 = ∅ )

Proof

Step	Hyp	Ref	Expression
1		fnrel	⊢ ( 𝐹 Fn ∅ → Rel 𝐹 )
2		fndm	⊢ ( 𝐹 Fn ∅ → dom 𝐹 = ∅ )
3		reldm0	⊢ ( Rel 𝐹 → ( 𝐹 = ∅ ↔ dom 𝐹 = ∅ ) )
4	3	biimpar	⊢ ( ( Rel 𝐹 ∧ dom 𝐹 = ∅ ) → 𝐹 = ∅ )
5	1 2 4	syl2anc	⊢ ( 𝐹 Fn ∅ → 𝐹 = ∅ )
6		fun0	⊢ Fun ∅
7		dm0	⊢ dom ∅ = ∅
8		df-fn	⊢ ( ∅ Fn ∅ ↔ ( Fun ∅ ∧ dom ∅ = ∅ ) )
9	6 7 8	mpbir2an	⊢ ∅ Fn ∅
10		fneq1	⊢ ( 𝐹 = ∅ → ( 𝐹 Fn ∅ ↔ ∅ Fn ∅ ) )
11	9 10	mpbiri	⊢ ( 𝐹 = ∅ → 𝐹 Fn ∅ )
12	5 11	impbii	⊢ ( 𝐹 Fn ∅ ↔ 𝐹 = ∅ )