Theorem fnsnfv

Description: Singleton of function value. (Contributed by NM, 22-May-1998) (Proof shortened by Scott Fenton, 8-Aug-2024)

	Ref	Expression
Assertion	fnsnfv	|- ( ( F Fn A /\ B e. A ) -> { ( F ` B ) } = ( F " { B } ) )

Proof

Step	Hyp	Ref	Expression
1		imasng	|- ( B e. A -> ( F " { B } ) = { y | B F y } )
2	1	adantl	|- ( ( F Fn A /\ B e. A ) -> ( F " { B } ) = { y | B F y } )
3		velsn	|- ( y e. { ( F ` B ) } <-> y = ( F ` B ) )
4		eqcom	|- ( y = ( F ` B ) <-> ( F ` B ) = y )
5	3 4	bitri	|- ( y e. { ( F ` B ) } <-> ( F ` B ) = y )
6		fnbrfvb	|- ( ( F Fn A /\ B e. A ) -> ( ( F ` B ) = y <-> B F y ) )
7	5 6	bitr2id	|- ( ( F Fn A /\ B e. A ) -> ( B F y <-> y e. { ( F ` B ) } ) )
8	7	abbi1dv	|- ( ( F Fn A /\ B e. A ) -> { y | B F y } = { ( F ` B ) } )
9	2 8	eqtr2d	|- ( ( F Fn A /\ B e. A ) -> { ( F ` B ) } = ( F " { B } ) )