Definition df-s1 14520

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 14528, and not, as maybe expected, the empty word, see also s1nz 14531. (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 14519	. 2 class ⟨“𝐴”⟩
3		cc0 11026	. . . 4 class 0
4		cid 5518	. . . . 5 class I
5	1, 4	cfv 6492	. . . 4 class ( I ‘𝐴)
6	3, 5	cop 4586	. . 3 class ⟨0, ( I ‘𝐴)⟩
7	6	csn 4580	. 2 class {⟨0, ( I ‘𝐴)⟩}
8	2, 7	wceq 1541	1 wff ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}

This definition is referenced by:  ids1  14521  s1val  14522  s1eq  14524  s1len  14530  s1nz  14531  funcnvs1  14835