Theorem nelrnres

Description: If A is not in the range, it is not in the range of any restriction. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Assertion	nelrnres	$$⊢\neg A\in \mathrm{ran}B\to \neg A\in \mathrm{ran}\left({B\upharpoonright }_C\right)$$

Proof

Step	Hyp	Ref	Expression
1		rnresss	$$⊢\mathrm{ran}\left({B\upharpoonright }_C\right)\subseteq \mathrm{ran}B$$
2		ssnel	$$⊢\left(\mathrm{ran}\left({B\upharpoonright }_C\right)\subseteq \mathrm{ran}B\wedge \neg A\in \mathrm{ran}B\right)\to \neg A\in \mathrm{ran}\left({B\upharpoonright }_C\right)$$
3	1 2	mpan	$$⊢\neg A\in \mathrm{ran}B\to \neg A\in \mathrm{ran}\left({B\upharpoonright }_C\right)$$