Theorem s1cli

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

	Ref	Expression
Assertion	s1cli	$$⊢⟨“A”⟩\in \mathrm{Word}\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		ids1	$$⊢⟨“A”⟩=⟨“\mathrm{I}\left(A\right)”⟩$$
2		fvex	$$⊢\mathrm{I}\left(A\right)\in \mathrm{V}$$
3		s1cl	$$⊢\mathrm{I}\left(A\right)\in \mathrm{V}\to ⟨“\mathrm{I}\left(A\right)”⟩\in \mathrm{Word}\mathrm{V}$$
4	2 3	ax-mp	$$⊢⟨“\mathrm{I}\left(A\right)”⟩\in \mathrm{Word}\mathrm{V}$$
5	1 4	eqeltri	$$⊢⟨“A”⟩\in \mathrm{Word}\mathrm{V}$$