Definition df-s1 14644

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 14652, and not, as maybe expected, the empty word, see also s1nz 14655. (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 14643	. 2 class ⟨“𝐴”⟩
3		cc0 11184	. . . 4 class 0
4		cid 5592	. . . . 5 class I
5	1, 4	cfv 6573	. . . 4 class ( I ‘𝐴)
6	3, 5	cop 4654	. . 3 class ⟨0, ( I ‘𝐴)⟩
7	6	csn 4648	. 2 class {⟨0, ( I ‘𝐴)⟩}
8	2, 7	wceq 1537	1 wff ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}

This definition is referenced by:  ids1  14645  s1val  14646  s1eq  14648  s1len  14654  s1nz  14655  funcnvs1  14961