Definition df-s1 14229

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 14237, and not, as maybe expected, the empty word, see also s1nz 14240. (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 14228	. 2 class ⟨“𝐴”⟩
3		cc0 10802	. . . 4 class 0
4		cid 5479	. . . . 5 class I
5	1, 4	cfv 6418	. . . 4 class ( I ‘𝐴)
6	3, 5	cop 4564	. . 3 class ⟨0, ( I ‘𝐴)⟩
7	6	csn 4558	. 2 class {⟨0, ( I ‘𝐴)⟩}
8	2, 7	wceq 1539	1 wff ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}

This definition is referenced by:  ids1  14230  s1val  14231  s1eq  14233  s1len  14239  s1nz  14240  funcnvs1  14553