Theorem elsetpreimafvb

Description: The characterization of an element of the class P of all preimages of function values. (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	elsetpreimafvb	$$⊢S\in V\to \left(S\in P\leftrightarrow \exists x\in AS=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\right)$$

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	1	eleq2i	$$⊢S\in P\leftrightarrow S\in \left\{z|\exists x\in Az=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\right\}$$
3		eqeq1	$$⊢z=S\to \left(z=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\leftrightarrow S=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\right)$$
4	3	rexbidv	$$⊢z=S\to \left(\exists x\in Az=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\leftrightarrow \exists x\in AS=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\right)$$
5	4	elabg	$$⊢S\in V\to \left(S\in \left\{z|\exists x\in Az=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\right\}\leftrightarrow \exists x\in AS=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\right)$$
6	2 5	bitrid	$$⊢S\in V\to \left(S\in P\leftrightarrow \exists x\in AS=F^{-1}\left[\left\{F\left(x\right)\right\}\right]\right)$$