Theorem s1rn

Description: The range of a singleton word. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Assertion	s1rn	$$⊢A\in V\to \mathrm{ran}⟨“A”⟩=\left\{A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		s1val	$$⊢A\in V\to ⟨“A”⟩=\left\{⟨0,A⟩\right\}$$
2	1	rneqd	$$⊢A\in V\to \mathrm{ran}⟨“A”⟩=\mathrm{ran}\left\{⟨0,A⟩\right\}$$
3		c0ex	$$⊢0\in \mathrm{V}$$
4	3	rnsnop	$$⊢\mathrm{ran}\left\{⟨0,A⟩\right\}=\left\{A\right\}$$
5	2 4	eqtrdi	$$⊢A\in V\to \mathrm{ran}⟨“A”⟩=\left\{A\right\}$$