Definition df-s1 14524

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 14532, and not, as maybe expected, the empty word, see also s1nz 14535. (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 14523	. 2 class ⟨“𝐴”⟩
3		cc0 11030	. . . 4 class 0
4		cid 5519	. . . . 5 class I
5	1, 4	cfv 6493	. . . 4 class ( I ‘𝐴)
6	3, 5	cop 4587	. . 3 class ⟨0, ( I ‘𝐴)⟩
7	6	csn 4581	. 2 class {⟨0, ( I ‘𝐴)⟩}
8	2, 7	wceq 1542	1 wff ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}

This definition is referenced by:  ids1  14525  s1val  14526  s1eq  14528  s1len  14534  s1nz  14535  funcnvs1  14839