Theorem s1rn

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

	Ref	Expression
Assertion	s1rn	⊢ ( 𝐴 ∈ 𝑉 → ran ⟨“ 𝐴 ”⟩ = { 𝐴 } )

Proof

Step	Hyp	Ref	Expression
1		s1val	⊢ ( 𝐴 ∈ 𝑉 → ⟨“ 𝐴 ”⟩ = { ⟨ 0 , 𝐴 ⟩ } )
2	1	rneqd	⊢ ( 𝐴 ∈ 𝑉 → ran ⟨“ 𝐴 ”⟩ = ran { ⟨ 0 , 𝐴 ⟩ } )
3		c0ex	⊢ 0 ∈ V
4	3	rnsnop	⊢ ran { ⟨ 0 , 𝐴 ⟩ } = { 𝐴 }
5	2 4	eqtrdi	⊢ ( 𝐴 ∈ 𝑉 → ran ⟨“ 𝐴 ”⟩ = { 𝐴 } )