Definition df-s1 14630

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 14638, and not, as maybe expected, the empty word, see also s1nz 14641. (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 14629	. 2 class ⟨“𝐴”⟩
3		cc0 11096	. . . 4 class 0
4		cid 5553	. . . . 5 class I
5	1, 4	cfv 6534	. . . 4 class ( I ‘𝐴)
6	3, 5	cop 4597	. . 3 class ⟨0, ( I ‘𝐴)⟩
7	6	csn 4591	. 2 class {⟨0, ( I ‘𝐴)⟩}
8	2, 7	wceq 1567	1 wff ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}

This definition is referenced by:  ids1  14631  s1val  14632  s1eq  14634  s1len  14640  s1nz  14641  funcnvs1  14945