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 \land A \in dom F) \to ran ({F ↾}_{\{A\}}) = \{F (A)\}$

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

Metamath Proof Explorer