Definition df-s1 14543

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 14551, and not, as maybe expected, the empty word, see also s1nz 14554. (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 14542	. 2 class ⟨“𝐴”⟩
3		cc0 11107	. . . 4 class 0
4		cid 5573	. . . . 5 class I
5	1, 4	cfv 6541	. . . 4 class ( I ‘𝐴)
6	3, 5	cop 4634	. . 3 class ⟨0, ( I ‘𝐴)⟩
7	6	csn 4628	. 2 class {⟨0, ( I ‘𝐴)⟩}
8	2, 7	wceq 1542	1 wff ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}

This definition is referenced by:  ids1  14544  s1val  14545  s1eq  14547  s1len  14553  s1nz  14554  funcnvs1  14860