Definition df-s1 14634

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 14642, and not, as maybe expected, the empty word, see also s1nz 14645. (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 14633	. 2 class ⟨“𝐴”⟩
3		cc0 11155	. . . 4 class 0
4		cid 5577	. . . . 5 class I
5	1, 4	cfv 6561	. . . 4 class ( I ‘𝐴)
6	3, 5	cop 4632	. . 3 class ⟨0, ( I ‘𝐴)⟩
7	6	csn 4626	. 2 class {⟨0, ( I ‘𝐴)⟩}
8	2, 7	wceq 1540	1 wff ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}

This definition is referenced by:  ids1  14635  s1val  14636  s1eq  14638  s1len  14644  s1nz  14645  funcnvs1  14951