Theorem elsetpreimafveqfv

Description: The elements of the preimage of a function value have the same function values. (Contributed by AV, 5-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	elsetpreimafveqfv	$$⊢\left(FFnA\wedge \left(S\in P\wedge X\in S\wedge Y\in S\right)\right)\to F\left(X\right)=F\left(Y\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		simpr	$$⊢\left(Y\in A\wedge F\left(Y\right)=F\left(X\right)\right)\to F\left(Y\right)=F\left(X\right)$$
4	3	eqcomd	$$⊢\left(Y\in A\wedge F\left(Y\right)=F\left(X\right)\right)\to F\left(X\right)=F\left(Y\right)$$
5	2 4	biimtrdi	$$⊢\left(FFnA\wedge S\in P\wedge X\in S\right)\to \left(Y\in S\to F\left(X\right)=F\left(Y\right)\right)$$
6	5	3exp	$$⊢FFnA\to \left(S\in P\to \left(X\in S\to \left(Y\in S\to F\left(X\right)=F\left(Y\right)\right)\right)\right)$$
7	6	3imp2	$$⊢\left(FFnA\wedge \left(S\in P\wedge X\in S\wedge Y\in S\right)\right)\to F\left(X\right)=F\left(Y\right)$$