Definition df-s1 14750

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 14758, and not, as maybe expected, the empty word, see also s1nz 14761. (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 14749	. 2 class ⟨“𝐴”⟩
3		cc0 11207	. . . 4 class 0
4		cid 5545	. . . . 5 class I
5	1, 4	cfv 6543	. . . 4 class ( I ‘𝐴)
6	3, 5	cop 4834	. . 3 class ⟨0, ( I ‘𝐴)⟩
7	6	csn 4584	. 2 class {⟨0, ( I ‘𝐴)⟩}
8	2, 7	wceq 1569	1 wff ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}

This definition is used by:  ids1  14751  s1val  14752  s1eq  14754  s1len  14760  s1nz  14761  funcnvs1  15072