Definition df-s1 14663

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 14671, and not, as maybe expected, the empty word, see also s1nz 14674. (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 14662	. 2 class ⟨“𝐴”⟩
3		cc0 11124	. . . 4 class 0
4		cid 5549	. . . . 5 class I
5	1, 4	cfv 6533	. . . 4 class ( I ‘𝐴)
6	3, 5	cop 4590	. . 3 class ⟨0, ( I ‘𝐴)⟩
7	6	csn 4584	. 2 class {⟨0, ( I ‘𝐴)⟩}
8	2, 7	wceq 1570	1 wff ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}

This definition is used by:  ids1  14664  s1val  14665  s1eq  14667  s1len  14673  s1nz  14674  funcnvs1  14983