Metamath Proof Explorer


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