Theorem rnfvprc

Description: The range of a function value at a proper class is empty. (Contributed by AV, 20-Aug-2022)

	Ref	Expression
Hypothesis	rnfvprc.y	$$⊢Y=F\left(X\right)$$
Assertion	rnfvprc	$$⊢\neg X\in \mathrm{V}\to \mathrm{ran}Y=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		rnfvprc.y	$$⊢Y=F\left(X\right)$$
2		fvprc	$$⊢\neg X\in \mathrm{V}\to F\left(X\right)=\varnothing$$
3	1 2	eqtrid	$$⊢\neg X\in \mathrm{V}\to Y=\varnothing$$
4	3	rneqd	$$⊢\neg X\in \mathrm{V}\to \mathrm{ran}Y=\mathrm{ran}\varnothing$$
5		rn0	$$⊢\mathrm{ran}\varnothing =\varnothing$$
6	4 5	eqtrdi	$$⊢\neg X\in \mathrm{V}\to \mathrm{ran}Y=\varnothing$$