Definition df-s1 14506

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 14514, and not, as maybe expected, the empty word, see also s1nz 14517. (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 14505	. 2 class ⟨“𝐴”⟩
3		cc0 11013	. . . 4 class 0
4		cid 5513	. . . . 5 class I
5	1, 4	cfv 6486	. . . 4 class ( I ‘𝐴)
6	3, 5	cop 4581	. . 3 class ⟨0, ( I ‘𝐴)⟩
7	6	csn 4575	. 2 class {⟨0, ( I ‘𝐴)⟩}
8	2, 7	wceq 1541	1 wff ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}

This definition is referenced by:  ids1  14507  s1val  14508  s1eq  14510  s1len  14516  s1nz  14517  funcnvs1  14821