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	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
	fnimasnd.2	⊢ ( 𝜑 → 𝑆 ∈ 𝐴 )
Assertion	fnimasnd	⊢ ( 𝜑 → ( 𝐹 “ { 𝑆 } ) = { ( 𝐹 ‘ 𝑆 ) } )

Proof

Step	Hyp	Ref	Expression
1		fnimasnd.1	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
2		fnimasnd.2	⊢ ( 𝜑 → 𝑆 ∈ 𝐴 )
3		fnsnfv	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝐴 ) → { ( 𝐹 ‘ 𝑆 ) } = ( 𝐹 “ { 𝑆 } ) )
4	1 2 3	syl2anc	⊢ ( 𝜑 → { ( 𝐹 ‘ 𝑆 ) } = ( 𝐹 “ { 𝑆 } ) )
5	4	eqcomd	⊢ ( 𝜑 → ( 𝐹 “ { 𝑆 } ) = { ( 𝐹 ‘ 𝑆 ) } )