Definition df-s1 11144

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 11151, and not, as maybe expected, the empty word. (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 11143	. 2 class ⟨“𝐴”⟩
3		cc0 7995	. . . 4 class 0
4		cid 4378	. . . . 5 class I
5	1, 4	cfv 5317	. . . 4 class ( I ‘𝐴)
6	3, 5	cop 3669	. . 3 class ⟨0, ( I ‘𝐴)⟩
7	6	csn 3666	. 2 class {⟨0, ( I ‘𝐴)⟩}
8	2, 7	wceq 1395	1 wff ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}

This definition is referenced by:  s1val  11145  s1eq  11147  s1prc  11151