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 ( 𝐹 ↾ { 𝐴 } ) = { ( 𝐹 ‘ 𝐴 ) } )