Theorem s1cli

Description: A singleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016)

	Ref	Expression
Assertion	s1cli	⊢ ⟨“ 𝐴 ”⟩ ∈ Word V

Proof

Step	Hyp	Ref	Expression
1		ids1	⊢ ⟨“ 𝐴 ”⟩ = ⟨“ ( I ‘ 𝐴 ) ”⟩
2		fvex	⊢ ( I ‘ 𝐴 ) ∈ V
3		s1cl	⊢ ( ( I ‘ 𝐴 ) ∈ V → ⟨“ ( I ‘ 𝐴 ) ”⟩ ∈ Word V )
4	2 3	ax-mp	⊢ ⟨“ ( I ‘ 𝐴 ) ”⟩ ∈ Word V
5	1 4	eqeltri	⊢ ⟨“ 𝐴 ”⟩ ∈ Word V