Definition df-s1 13950

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 13958, and not, as maybe expected, the empty word, see also s1nz 13961. (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 13949	. 2 class ⟨“𝐴”⟩
3		cc0 10537	. . . 4 class 0
4		cid 5459	. . . . 5 class I
5	1, 4	cfv 6355	. . . 4 class ( I ‘𝐴)
6	3, 5	cop 4573	. . 3 class ⟨0, ( I ‘𝐴)⟩
7	6	csn 4567	. 2 class {⟨0, ( I ‘𝐴)⟩}
8	2, 7	wceq 1537	1 wff ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}

This definition is referenced by:  ids1  13951  s1val  13952  s1eq  13954  s1len  13960  s1nz  13961  funcnvs1  14274