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	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → { ( 𝐹 ‘ 𝐵 ) } = ( 𝐹 “ { 𝐵 } ) )

Proof

Step	Hyp	Ref	Expression
1		imasng	⊢ ( 𝐵 ∈ 𝐴 → ( 𝐹 “ { 𝐵 } ) = { 𝑦 ∣ 𝐵 𝐹 𝑦 } )
2	1	adantl	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝐹 “ { 𝐵 } ) = { 𝑦 ∣ 𝐵 𝐹 𝑦 } )
3		velsn	⊢ ( 𝑦 ∈ { ( 𝐹 ‘ 𝐵 ) } ↔ 𝑦 = ( 𝐹 ‘ 𝐵 ) )
4		eqcom	⊢ ( 𝑦 = ( 𝐹 ‘ 𝐵 ) ↔ ( 𝐹 ‘ 𝐵 ) = 𝑦 )
5	3 4	bitri	⊢ ( 𝑦 ∈ { ( 𝐹 ‘ 𝐵 ) } ↔ ( 𝐹 ‘ 𝐵 ) = 𝑦 )
6		fnbrfvb	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝐵 ) = 𝑦 ↔ 𝐵 𝐹 𝑦 ) )
7	5 6	bitr2id	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝐵 𝐹 𝑦 ↔ 𝑦 ∈ { ( 𝐹 ‘ 𝐵 ) } ) )
8	7	eqabcdv	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → { 𝑦 ∣ 𝐵 𝐹 𝑦 } = { ( 𝐹 ‘ 𝐵 ) } )
9	2 8	eqtr2d	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → { ( 𝐹 ‘ 𝐵 ) } = ( 𝐹 “ { 𝐵 } ) )