This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem s1cli

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

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

Proof

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