Theorem elsetpreimafvrab

Description: An element of the preimage of a function value expressed as a restricted class abstraction. (Contributed by AV, 9-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	elsetpreimafvrab	$$⊢\left(FFnA\wedge S\in P\wedge X\in S\right)\to S=\left\{x\in A|F\left(x\right)=F\left(X\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	elsetpreimafvbi	$$⊢\left(FFnA\wedge S\in P\wedge X\in S\right)\to \left(y\in S\leftrightarrow \left(y\in A\wedge F\left(y\right)=F\left(X\right)\right)\right)$$
3		fveqeq2	$$⊢x=y\to \left(F\left(x\right)=F\left(X\right)\leftrightarrow F\left(y\right)=F\left(X\right)\right)$$
4	3	elrab	$$⊢y\in \left\{x\in A|F\left(x\right)=F\left(X\right)\right\}\leftrightarrow \left(y\in A\wedge F\left(y\right)=F\left(X\right)\right)$$
5	2 4	bitr4di	$$⊢\left(FFnA\wedge S\in P\wedge X\in S\right)\to \left(y\in S\leftrightarrow y\in \left\{x\in A|F\left(x\right)=F\left(X\right)\right\}\right)$$
6	5	eqrdv	$$⊢\left(FFnA\wedge S\in P\wedge X\in S\right)\to S=\left\{x\in A|F\left(x\right)=F\left(X\right)\right\}$$