Definition df-s1 14568

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 14576, and not, as maybe expected, the empty word, see also s1nz 14579. (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 14567	. 2 class ⟨“𝐴”⟩
3		cc0 11075	. . . 4 class 0
4		cid 5535	. . . . 5 class I
5	1, 4	cfv 6514	. . . 4 class ( I ‘𝐴)
6	3, 5	cop 4598	. . 3 class ⟨0, ( I ‘𝐴)⟩
7	6	csn 4592	. 2 class {⟨0, ( I ‘𝐴)⟩}
8	2, 7	wceq 1540	1 wff ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}

This definition is referenced by:  ids1  14569  s1val  14570  s1eq  14572  s1len  14578  s1nz  14579  funcnvs1  14885