Theorem afv2prc

Description: A function's value at a proper class is not defined, compare with fvprc . (Contributed by AV, 5-Sep-2022)

	Ref	Expression
Assertion	afv2prc	$$⊢\neg A\in \mathrm{V}\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F$$

Proof

Step	Hyp	Ref	Expression
1		prcnel	$$⊢\neg A\in \mathrm{V}\to \neg A\in \mathrm{dom}F$$
2		ndmafv2nrn	$$⊢\neg A\in \mathrm{dom}F\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F$$
3	1 2	syl	$$⊢\neg A\in \mathrm{V}\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\notin \mathrm{ran}F$$