Definition df-s1 14550

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 14558, and not, as maybe expected, the empty word, see also s1nz 14561. (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 14549	. 2 class ⟨“𝐴”⟩
3		cc0 11029	. . . 4 class 0
4		cid 5512	. . . . 5 class I
5	1, 4	cfv 6485	. . . 4 class ( I ‘𝐴)
6	3, 5	cop 4561	. . 3 class ⟨0, ( I ‘𝐴)⟩
7	6	csn 4555	. 2 class {⟨0, ( I ‘𝐴)⟩}
8	2, 7	wceq 1547	1 wff ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}

This definition is referenced by:  ids1  14551  s1val  14552  s1eq  14554  s1len  14560  s1nz  14561  funcnvs1  14865