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

Metamath Proof Explorer

Theorem rnressnsn

Description: The range of a restriction to a singleton is a singleton. See dmressnsn . (Contributed by Thierry Arnoux, 25-Jan-2026)

Ref Expression
Assertion rnressnsn ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ran ( 𝐹 ↾ { 𝐴 } ) = { ( 𝐹 ‘ 𝐴 ) } )

Proof

Step Hyp Ref Expression
1 funfn ⊢ ( Fun 𝐹 ↔ 𝐹 Fn dom 𝐹 )
2 fnressn ⊢ ( ( 𝐹 Fn dom 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( 𝐹 ↾ { 𝐴 } ) = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } )
3 1 2 sylanb ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( 𝐹 ↾ { 𝐴 } ) = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } )
4 3 rneqd ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ran ( 𝐹 ↾ { 𝐴 } ) = ran { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } )
5 rnsnopg ⊢ ( 𝐴 ∈ dom 𝐹 → ran { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } = { ( 𝐹 ‘ 𝐴 ) } )
6 5 adantl ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ran { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } = { ( 𝐹 ‘ 𝐴 ) } )
7 4 6 eqtrd ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ran ( 𝐹 ↾ { 𝐴 } ) = { ( 𝐹 ‘ 𝐴 ) } )