Theorem 0fv

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

	Ref	Expression
Assertion	0fv	$$⊢\varnothing \left(A\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		noel	$$⊢\neg A\in \varnothing$$
2		dm0	$$⊢\mathrm{dom}\varnothing =\varnothing$$
3	2	eleq2i	$$⊢A\in \mathrm{dom}\varnothing \leftrightarrow A\in \varnothing$$
4	1 3	mtbir	$$⊢\neg A\in \mathrm{dom}\varnothing$$
5		ndmfv	$$⊢\neg A\in \mathrm{dom}\varnothing \to \varnothing \left(A\right)=\varnothing$$
6	4 5	ax-mp	$$⊢\varnothing \left(A\right)=\varnothing$$