Definition df-s1 14784

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 14792, and not, as maybe expected, the empty word, see also s1nz 14795. (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 14783	. 2 class ⟨“𝐴”⟩
3		cc0 11239	. . . 4 class 0
4		cid 5552	. . . . 5 class I
5	1, 4	cfv 6566	. . . 4 class ( I ‘𝐴)
6	3, 5	cop 4840	. . 3 class ⟨0, ( I ‘𝐴)⟩
7	6	csn 4588	. 2 class {⟨0, ( I ‘𝐴)⟩}
8	2, 7	wceq 1570	1 wff ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}

This definition is used by:  ids1  14785  s1val  14786  s1eq  14788  s1len  14794  s1nz  14795  funcnvs1  15106