Theorem setpreimafvex

Description: The class P of all preimages of function values is a set. (Contributed by AV, 10-Mar-2024)

	Ref	Expression
Hypothesis	setpreimafvex.p	$$⊢P=\left\{z|\exists x\in Az=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\right\}$$
Assertion	setpreimafvex	$$⊢A\in V\to P\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		setpreimafvex.p	$$⊢P=\left\{z|\exists x\in Az=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\right\}$$
2		abrexexg	$$⊢A\in V\to \left\{z|\exists x\in Az=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\right\}\in \mathrm{V}$$
3	1 2	eqeltrid	$$⊢A\in V\to P\in \mathrm{V}$$