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 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 ) } )