Metamath Proof Explorer

Theorem eqfvelsetpreimafv

Description: If an element of the domain of the function has the same function value as an element of the preimage of a function value, then it is an element of the same preimage. (Contributed by AV, 9-Mar-2024)

		Ref	Expression
	Hypothesis	setpreimafvex.p	\|- P = { z \| E. x e. A z = ( `' F " { ( F ` x ) } ) }
	Assertion	eqfvelsetpreimafv	\|- ( ( F Fn A /\ S e. P /\ X e. S ) -> ( ( Y e. A /\ ( F ` Y ) = ( F ` X ) ) -> Y e. S ) )

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	2	biimprd	\|- ( ( F Fn A /\ S e. P /\ X e. S ) -> ( ( Y e. A /\ ( F ` Y ) = ( F ` X ) ) -> Y e. S ) )

Step

Hyp

Ref

Expression

setpreimafvex.p

 |-  P = { z | E. x e. A z = ( `' F " { ( F ` x ) } ) }

elsetpreimafvbi

 |-  ( ( F Fn A /\ S e. P /\ X e. S ) -> ( Y e. S <-> ( Y e. A /\ ( F ` Y ) = ( F ` X ) ) ) )

biimprd

 |-  ( ( F Fn A /\ S e. P /\ X e. S ) -> ( ( Y e. A /\ ( F ` Y ) = ( F ` X ) ) -> Y e. S ) )