Theorem fnsnfv

Description: Singleton of function value. (Contributed by NM, 22-May-1998)

	Ref	Expression
Assertion	fnsnfv	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → { ( 𝐹 ‘ 𝐵 ) } = ( 𝐹 “ { 𝐵 } ) )

Proof

Step	Hyp	Ref	Expression
1		eqcom	⊢ ( 𝑦 = ( 𝐹 ‘ 𝐵 ) ↔ ( 𝐹 ‘ 𝐵 ) = 𝑦 )
2		fnbrfvb	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝐵 ) = 𝑦 ↔ 𝐵 𝐹 𝑦 ) )
3	1 2	syl5bb	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝑦 = ( 𝐹 ‘ 𝐵 ) ↔ 𝐵 𝐹 𝑦 ) )
4	3	abbidv	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → { 𝑦 ∣ 𝑦 = ( 𝐹 ‘ 𝐵 ) } = { 𝑦 ∣ 𝐵 𝐹 𝑦 } )
5		df-sn	⊢ { ( 𝐹 ‘ 𝐵 ) } = { 𝑦 ∣ 𝑦 = ( 𝐹 ‘ 𝐵 ) }
6	5	a1i	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → { ( 𝐹 ‘ 𝐵 ) } = { 𝑦 ∣ 𝑦 = ( 𝐹 ‘ 𝐵 ) } )
7		fnrel	⊢ ( 𝐹 Fn 𝐴 → Rel 𝐹 )
8		relimasn	⊢ ( Rel 𝐹 → ( 𝐹 “ { 𝐵 } ) = { 𝑦 ∣ 𝐵 𝐹 𝑦 } )
9	7 8	syl	⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 “ { 𝐵 } ) = { 𝑦 ∣ 𝐵 𝐹 𝑦 } )
10	9	adantr	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝐹 “ { 𝐵 } ) = { 𝑦 ∣ 𝐵 𝐹 𝑦 } )
11	4 6 10	3eqtr4d	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → { ( 𝐹 ‘ 𝐵 ) } = ( 𝐹 “ { 𝐵 } ) )