Theorem s1rn

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

	Ref	Expression
Assertion	s1rn	|- ( A e. V -> ran <" A "> = { A } )

Proof

Step	Hyp	Ref	Expression
1		s1val	|- ( A e. V -> <" A "> = { <. 0 , A >. } )
2	1	rneqd	|- ( A e. V -> ran <" A "> = ran { <. 0 , A >. } )
3		c0ex	|- 0 e. _V
4	3	rnsnop	|- ran { <. 0 , A >. } = { A }
5	2 4	eqtrdi	|- ( A e. V -> ran <" A "> = { A } )