Metamath Proof Explorer


Theorem s1cli

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

Ref Expression
Assertion s1cli ⟨“A”⟩WordV

Proof

Step Hyp Ref Expression
1 ids1 ⟨“A”⟩=⟨“IA”⟩
2 fvex IAV
3 s1cl IAV⟨“IA”⟩WordV
4 2 3 ax-mp ⟨“IA”⟩WordV
5 1 4 eqeltri ⟨“A”⟩WordV