Definition df-s1 14561

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 14569, and not, as maybe expected, the empty word, see also s1nz 14572. (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 14560	. 2 class ⟨“𝐴”⟩
3		cc0 11068	. . . 4 class 0
4		cid 5532	. . . . 5 class I
5	1, 4	cfv 6511	. . . 4 class ( I ‘𝐴)
6	3, 5	cop 4595	. . 3 class ⟨0, ( I ‘𝐴)⟩
7	6	csn 4589	. 2 class {⟨0, ( I ‘𝐴)⟩}
8	2, 7	wceq 1540	1 wff ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}

This definition is referenced by:  ids1  14562  s1val  14563  s1eq  14565  s1len  14571  s1nz  14572  funcnvs1  14878