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 F /\ A e. dom F ) -> ran ( F |` { A } ) = { ( F ` A ) } )

Proof

Step	Hyp	Ref	Expression
1		funfn	|- ( Fun F <-> F Fn dom F )
2		fnressn	|- ( ( F Fn dom F /\ A e. dom F ) -> ( F |` { A } ) = { <. A , ( F ` A ) >. } )
3	1 2	sylanb	|- ( ( Fun F /\ A e. dom F ) -> ( F |` { A } ) = { <. A , ( F ` A ) >. } )
4	3	rneqd	|- ( ( Fun F /\ A e. dom F ) -> ran ( F |` { A } ) = ran { <. A , ( F ` A ) >. } )
5		rnsnopg	|- ( A e. dom F -> ran { <. A , ( F ` A ) >. } = { ( F ` A ) } )
6	5	adantl	|- ( ( Fun F /\ A e. dom F ) -> ran { <. A , ( F ` A ) >. } = { ( F ` A ) } )
7	4 6	eqtrd	|- ( ( Fun F /\ A e. dom F ) -> ran ( F |` { A } ) = { ( F ` A ) } )