Metamath Proof Explorer


Definition df-s1

Description: Define the canonical injection from symbols to words. Although not required, A should usually be a set. Otherwise, the singleton word <" A "> would be the singleton word consisting of the empty set, see s1prc , and not, as maybe expected, the empty word, see also s1nz . (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by Mario Carneiro, 26-Feb-2016)

Ref Expression
Assertion df-s1 ⟨“A”⟩=0IA

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA classA
1 0 cs1 class⟨“A”⟩
2 cc0 class0
3 cid classI
4 0 3 cfv classIA
5 2 4 cop class0IA
6 5 csn class0IA
7 1 6 wceq wff⟨“A”⟩=0IA