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	$$⊢\left(\mathrm{Fun}F\wedge A\in \mathrm{dom}F\right)\to \mathrm{ran}\left({F\upharpoonright }_{\left\{A\right\}}\right)=\left\{F\left(A\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		funfn	$$⊢\mathrm{Fun}F\leftrightarrow FFn\mathrm{dom}F$$
2		fnressn	$$⊢\left(FFn\mathrm{dom}F\wedge A\in \mathrm{dom}F\right)\to {F\upharpoonright }_{\left\{A\right\}}=\left\{⟨A,F\left(A\right)⟩\right\}$$
3	1 2	sylanb	$$⊢\left(\mathrm{Fun}F\wedge A\in \mathrm{dom}F\right)\to {F\upharpoonright }_{\left\{A\right\}}=\left\{⟨A,F\left(A\right)⟩\right\}$$
4	3	rneqd	$$⊢\left(\mathrm{Fun}F\wedge A\in \mathrm{dom}F\right)\to \mathrm{ran}\left({F\upharpoonright }_{\left\{A\right\}}\right)=\mathrm{ran}\left\{⟨A,F\left(A\right)⟩\right\}$$
5		rnsnopg	$$⊢A\in \mathrm{dom}F\to \mathrm{ran}\left\{⟨A,F\left(A\right)⟩\right\}=\left\{F\left(A\right)\right\}$$
6	5	adantl	$$⊢\left(\mathrm{Fun}F\wedge A\in \mathrm{dom}F\right)\to \mathrm{ran}\left\{⟨A,F\left(A\right)⟩\right\}=\left\{F\left(A\right)\right\}$$
7	4 6	eqtrd	$$⊢\left(\mathrm{Fun}F\wedge A\in \mathrm{dom}F\right)\to \mathrm{ran}\left({F\upharpoonright }_{\left\{A\right\}}\right)=\left\{F\left(A\right)\right\}$$