Definition df-s1 14542

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 14550, and not, as maybe expected, the empty word, see also s1nz 14553. (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 14541	. 2 class ⟨“𝐴”⟩
3		cc0 11106	. . . 4 class 0
4		cid 5572	. . . . 5 class I
5	1, 4	cfv 6540	. . . 4 class ( I ‘𝐴)
6	3, 5	cop 4633	. . 3 class ⟨0, ( I ‘𝐴)⟩
7	6	csn 4627	. 2 class {⟨0, ( I ‘𝐴)⟩}
8	2, 7	wceq 1542	1 wff ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}

This definition is referenced by:  ids1  14543  s1val  14544  s1eq  14546  s1len  14552  s1nz  14553  funcnvs1  14859