Description: The range of a singleton word. (Contributed by Mario Carneiro, 18-Jul-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | s1rn | |- ( A e. V -> ran <" A "> = { A } ) |
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 } ) |