Definition df-s1 13794

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 13802, and not, as maybe expected, the empty word, see also s1nz 13805. (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 13793	. 2 class ⟨“𝐴”⟩
3		cc0 10383	. . . 4 class 0
4		cid 5347	. . . . 5 class I
5	1, 4	cfv 6225	. . . 4 class ( I ‘𝐴)
6	3, 5	cop 4478	. . 3 class ⟨0, ( I ‘𝐴)⟩
7	6	csn 4472	. 2 class {⟨0, ( I ‘𝐴)⟩}
8	2, 7	wceq 1522	1 wff ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}

This definition is referenced by:  ids1  13795  s1val  13796  s1eq  13798  s1len  13804  s1nz  13805  funcnvs1  14110