Theorem f0

Description: The empty function. (Contributed by NM, 14-Aug-1999)

	Ref	Expression
Assertion	f0	⊢ ∅ : ∅ ⟶ 𝐴

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ∅ = ∅
2		fn0	⊢ ( ∅ Fn ∅ ↔ ∅ = ∅ )
3	1 2	mpbir	⊢ ∅ Fn ∅
4		rn0	⊢ ran ∅ = ∅
5		0ss	⊢ ∅ ⊆ 𝐴
6	4 5	eqsstri	⊢ ran ∅ ⊆ 𝐴
7		df-f	⊢ ( ∅ : ∅ ⟶ 𝐴 ↔ ( ∅ Fn ∅ ∧ ran ∅ ⊆ 𝐴 ) )
8	3 6 7	mpbir2an	⊢ ∅ : ∅ ⟶ 𝐴