Definition df-s1 14612

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 14620, and not, as maybe expected, the empty word, see also s1nz 14623. (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 14611	. 2 class ⟨“𝐴”⟩
3		cc0 11127	. . . 4 class 0
4		cid 5547	. . . . 5 class I
5	1, 4	cfv 6530	. . . 4 class ( I ‘𝐴)
6	3, 5	cop 4607	. . 3 class ⟨0, ( I ‘𝐴)⟩
7	6	csn 4601	. 2 class {⟨0, ( I ‘𝐴)⟩}
8	2, 7	wceq 1540	1 wff ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}

This definition is referenced by:  ids1  14613  s1val  14614  s1eq  14616  s1len  14622  s1nz  14623  funcnvs1  14929