Definition df-s1 14310

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 14318, and not, as maybe expected, the empty word, see also s1nz 14321. (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 14309	. 2 class ⟨“𝐴”⟩
3		cc0 10880	. . . 4 class 0
4		cid 5489	. . . . 5 class I
5	1, 4	cfv 6437	. . . 4 class ( I ‘𝐴)
6	3, 5	cop 4568	. . 3 class ⟨0, ( I ‘𝐴)⟩
7	6	csn 4562	. 2 class {⟨0, ( I ‘𝐴)⟩}
8	2, 7	wceq 1539	1 wff ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}

This definition is referenced by:  ids1  14311  s1val  14312  s1eq  14314  s1len  14320  s1nz  14321  funcnvs1  14634