Theorem preimafvsnel

Description: The preimage of a function value at X contains X . (Contributed by AV, 7-Mar-2024)

	Ref	Expression
Assertion	preimafvsnel	|- ( ( F Fn A /\ X e. A ) -> X e. ( `' F " { ( F ` X ) } ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	|- ( ( F Fn A /\ X e. A ) -> X e. A )
2		eqidd	|- ( ( F Fn A /\ X e. A ) -> ( F ` X ) = ( F ` X ) )
3		fniniseg	|- ( F Fn A -> ( X e. ( `' F " { ( F ` X ) } ) <-> ( X e. A /\ ( F ` X ) = ( F ` X ) ) ) )
4	3	adantr	|- ( ( F Fn A /\ X e. A ) -> ( X e. ( `' F " { ( F ` X ) } ) <-> ( X e. A /\ ( F ` X ) = ( F ` X ) ) ) )
5	1 2 4	mpbir2and	|- ( ( F Fn A /\ X e. A ) -> X e. ( `' F " { ( F ` X ) } ) )