Definition df-s1 13998

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 14006, and not, as maybe expected, the empty word, see also s1nz 14009. (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 13997	. 2 class ⟨“𝐴”⟩
3		cc0 10576	. . . 4 class 0
4		cid 5430	. . . . 5 class I
5	1, 4	cfv 6336	. . . 4 class ( I ‘𝐴)
6	3, 5	cop 4529	. . 3 class ⟨0, ( I ‘𝐴)⟩
7	6	csn 4523	. 2 class {⟨0, ( I ‘𝐴)⟩}
8	2, 7	wceq 1539	1 wff ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}

This definition is referenced by:  ids1  13999  s1val  14000  s1eq  14002  s1len  14008  s1nz  14009  funcnvs1  14322