Theorem fnimasnd

Description: The image of a function by a singleton whose element is in the domain of the function. (Contributed by Steven Nguyen, 7-Jun-2023)

	Ref	Expression
Hypotheses	fnimasnd.1	|- ( ph -> F Fn A )
	fnimasnd.2	|- ( ph -> S e. A )
Assertion	fnimasnd	|- ( ph -> ( F " { S } ) = { ( F ` S ) } )

Proof

Step	Hyp	Ref	Expression
1		fnimasnd.1	|- ( ph -> F Fn A )
2		fnimasnd.2	|- ( ph -> S e. A )
3		fnsnfv	|- ( ( F Fn A /\ S e. A ) -> { ( F ` S ) } = ( F " { S } ) )
4	1 2 3	syl2anc	|- ( ph -> { ( F ` S ) } = ( F " { S } ) )
5	4	eqcomd	|- ( ph -> ( F " { S } ) = { ( F ` S ) } )