Definition df-s1 13944

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 13952, and not, as maybe expected, the empty word, see also s1nz 13955. (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 13943	. 2 class ⟨“𝐴”⟩
3		cc0 10531	. . . 4 class 0
4		cid 5453	. . . . 5 class I
5	1, 4	cfv 6349	. . . 4 class ( I ‘𝐴)
6	3, 5	cop 4566	. . 3 class ⟨0, ( I ‘𝐴)⟩
7	6	csn 4560	. 2 class {⟨0, ( I ‘𝐴)⟩}
8	2, 7	wceq 1533	1 wff ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}

This definition is referenced by:  ids1  13945  s1val  13946  s1eq  13948  s1len  13954  s1nz  13955  funcnvs1  14268