Definition df-s1 14559

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 14567, and not, as maybe expected, the empty word, see also s1nz 14570. (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 14558	. 2 class ⟨“𝐴”⟩
3		cc0 11038	. . . 4 class 0
4		cid 5525	. . . . 5 class I
5	1, 4	cfv 6498	. . . 4 class ( I ‘𝐴)
6	3, 5	cop 4573	. . 3 class ⟨0, ( I ‘𝐴)⟩
7	6	csn 4567	. 2 class {⟨0, ( I ‘𝐴)⟩}
8	2, 7	wceq 1542	1 wff ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}

This definition is referenced by:  ids1  14560  s1val  14561  s1eq  14563  s1len  14569  s1nz  14570  funcnvs1  14874