Theorem nfvres

Description: The value of a non-member of a restriction is the empty set. (An artifact of our function value definition.) (Contributed by NM, 13-Nov-1995)

	Ref	Expression
Assertion	nfvres	$$⊢\neg A\in B\to \left({F\upharpoonright }_B\right)\left(A\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		dmres	$$⊢\mathrm{dom}\left({F\upharpoonright }_B\right)=B\cap \mathrm{dom}F$$
2		inss1	$$⊢B\cap \mathrm{dom}F\subseteq B$$
3	1 2	eqsstri	$$⊢\mathrm{dom}\left({F\upharpoonright }_B\right)\subseteq B$$
4	3	sseli	$$⊢A\in \mathrm{dom}\left({F\upharpoonright }_B\right)\to A\in B$$
5		ndmfv	$$⊢\neg A\in \mathrm{dom}\left({F\upharpoonright }_B\right)\to \left({F\upharpoonright }_B\right)\left(A\right)=\varnothing$$
6	4 5	nsyl5	$$⊢\neg A\in B\to \left({F\upharpoonright }_B\right)\left(A\right)=\varnothing$$