Definition df-s1 14604

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 14612, and not, as maybe expected, the empty word, see also s1nz 14615. (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 14603	. 2 class ⟨“𝐴”⟩
3		cc0 11067	. . . 4 class 0
4		cid 5537	. . . . 5 class I
5	1, 4	cfv 6516	. . . 4 class ( I ‘𝐴)
6	3, 5	cop 4585	. . 3 class ⟨0, ( I ‘𝐴)⟩
7	6	csn 4579	. 2 class {⟨0, ( I ‘𝐴)⟩}
8	2, 7	wceq 1559	1 wff ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}

This definition is referenced by:  ids1  14605  s1val  14606  s1eq  14608  s1len  14614  s1nz  14615  funcnvs1  14919