This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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