Theorem fexafv2ex

Description: The alternate function value is always a set if the function (resp. the domain of the function) is a set. (Contributed by AV, 3-Sep-2022)

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

Proof

Step	Hyp	Ref	Expression
1		rnexg	$$⊢F\in V\to \mathrm{ran}F\in \mathrm{V}$$
2		afv2ex	$$⊢\mathrm{ran}F\in \mathrm{V}\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\in \mathrm{V}$$
3	1 2	syl	$$⊢F\in V\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\in \mathrm{V}$$