Theorem afv2ex

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

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

Proof

Step	Hyp	Ref	Expression
1		df-afv2	$$⊢\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)=if\left(F\mathrm{defAt}A,\left(\iota x|AFx\right),𝒫\bigcup \mathrm{ran}F\right)$$
2		iotaex	$$⊢\left(\iota x|AFx\right)\in \mathrm{V}$$
3	2	a1i	$$⊢\mathrm{ran}F\in V\to \left(\iota x|AFx\right)\in \mathrm{V}$$
4		uniexg	$$⊢\mathrm{ran}F\in V\to \bigcup \mathrm{ran}F\in \mathrm{V}$$
5	4	pwexd	$$⊢\mathrm{ran}F\in V\to 𝒫\bigcup \mathrm{ran}F\in \mathrm{V}$$
6	3 5	ifcld	$$⊢\mathrm{ran}F\in V\to if\left(F\mathrm{defAt}A,\left(\iota x|AFx\right),𝒫\bigcup \mathrm{ran}F\right)\in \mathrm{V}$$
7	1 6	eqeltrid	$$⊢\mathrm{ran}F\in V\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}A\right)\in \mathrm{V}$$