Definition df-s1 14501

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 14509, and not, as maybe expected, the empty word, see also s1nz 14512. (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 14500	. 2 class ⟨“𝐴”⟩
3		cc0 11003	. . . 4 class 0
4		cid 5510	. . . . 5 class I
5	1, 4	cfv 6481	. . . 4 class ( I ‘𝐴)
6	3, 5	cop 4582	. . 3 class ⟨0, ( I ‘𝐴)⟩
7	6	csn 4576	. 2 class {⟨0, ( I ‘𝐴)⟩}
8	2, 7	wceq 1541	1 wff ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}

This definition is referenced by:  ids1  14502  s1val  14503  s1eq  14505  s1len  14511  s1nz  14512  funcnvs1  14816