Definition df-s1 14649

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

Assertion

Ref	Expression
df-s1	⊢ ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}

Detailed syntax breakdown of Definition df-s1

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	cs1 14648	. 2 class ⟨“𝐴”⟩
3		cc0 11111	. . . 4 class 0
4		cid 5557	. . . . 5 class I
5	1, 4	cfv 6540	. . . 4 class ( I ‘𝐴)
6	3, 5	cop 4597	. . 3 class ⟨0, ( I ‘𝐴)⟩
7	6	csn 4591	. 2 class {⟨0, ( I ‘𝐴)⟩}
8	2, 7	wceq 1570	1 wff ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}

This definition is used by:  ids1  14650  s1val  14651  s1eq  14653  s1len  14659  s1nz  14660  funcnvs1  14969