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 = { z | E. x e. A z = ( `' F " { ( F ` x ) } ) }
Assertion	elsetpreimafveqfv	|- ( ( F Fn A /\ ( S e. P /\ X e. S /\ Y e. S ) ) -> ( F ` X ) = ( F ` Y ) )

Proof

Step	Hyp	Ref	Expression
1		setpreimafvex.p	|- P = { z | E. x e. A z = ( `' F " { ( F ` x ) } ) }
2	1	elsetpreimafvbi	|- ( ( F Fn A /\ S e. P /\ X e. S ) -> ( Y e. S <-> ( Y e. A /\ ( F ` Y ) = ( F ` X ) ) ) )
3		simpr	|- ( ( Y e. A /\ ( F ` Y ) = ( F ` X ) ) -> ( F ` Y ) = ( F ` X ) )
4	3	eqcomd	|- ( ( Y e. A /\ ( F ` Y ) = ( F ` X ) ) -> ( F ` X ) = ( F ` Y ) )
5	2 4	biimtrdi	|- ( ( F Fn A /\ S e. P /\ X e. S ) -> ( Y e. S -> ( F ` X ) = ( F ` Y ) ) )
6	5	3exp	|- ( F Fn A -> ( S e. P -> ( X e. S -> ( Y e. S -> ( F ` X ) = ( F ` Y ) ) ) ) )
7	6	3imp2	|- ( ( F Fn A /\ ( S e. P /\ X e. S /\ Y e. S ) ) -> ( F ` X ) = ( F ` Y ) )