Theorem ndmfv

Description: The value of a class outside its domain is the empty set. (An artifact of our function value definition.) (Contributed by NM, 24-Aug-1995)

	Ref	Expression
Assertion	ndmfv	$$⊢\neg A\in \mathrm{dom}F\to F\left(A\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		euex	$$⊢\exists !xAFx\to \exists xAFx$$
2		eldmg	$$⊢A\in \mathrm{V}\to \left(A\in \mathrm{dom}F\leftrightarrow \exists xAFx\right)$$
3	1 2	imbitrrid	$$⊢A\in \mathrm{V}\to \left(\exists !xAFx\to A\in \mathrm{dom}F\right)$$
4	3	con3d	$$⊢A\in \mathrm{V}\to \left(\neg A\in \mathrm{dom}F\to \neg \exists !xAFx\right)$$
5		tz6.12-2	$$⊢\neg \exists !xAFx\to F\left(A\right)=\varnothing$$
6	4 5	syl6	$$⊢A\in \mathrm{V}\to \left(\neg A\in \mathrm{dom}F\to F\left(A\right)=\varnothing \right)$$
7		fvprc	$$⊢\neg A\in \mathrm{V}\to F\left(A\right)=\varnothing$$
8	7	a1d	$$⊢\neg A\in \mathrm{V}\to \left(\neg A\in \mathrm{dom}F\to F\left(A\right)=\varnothing \right)$$
9	6 8	pm2.61i	$$⊢\neg A\in \mathrm{dom}F\to F\left(A\right)=\varnothing$$