Theorem 0fv

Description: Function value of the empty set. (Contributed by Stefan O'Rear, 26-Nov-2014)

	Ref	Expression
Assertion	0fv	⊢ ( ∅ ‘ 𝐴 ) = ∅

Proof

Step	Hyp	Ref	Expression
1		noel	⊢ ¬ 𝐴 ∈ ∅
2		dm0	⊢ dom ∅ = ∅
3	2	eleq2i	⊢ ( 𝐴 ∈ dom ∅ ↔ 𝐴 ∈ ∅ )
4	1 3	mtbir	⊢ ¬ 𝐴 ∈ dom ∅
5		ndmfv	⊢ ( ¬ 𝐴 ∈ dom ∅ → ( ∅ ‘ 𝐴 ) = ∅ )
6	4 5	ax-mp	⊢ ( ∅ ‘ 𝐴 ) = ∅