Definition df-s1 11093

Description: Define the canonical injection from symbols to words. Although not required, A should usually be a set. Otherwise, the singleton word <" A "> would be the singleton word consisting of the empty set, see s1prc 11100, and not, as maybe expected, the empty word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)

Assertion

Ref	Expression
df-s1	|- <" A "> = { <. 0 , ( _I ` A ) >. }

Detailed syntax breakdown of Definition df-s1

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	cs1 11092	. 2 class <" A ">
3		cc0 7945	. . . 4 class 0
4		cid 4343	. . . . 5 class _I
5	1, 4	cfv 5280	. . . 4 class ( _I ` A )
6	3, 5	cop 3641	. . 3 class <. 0 , ( _I ` A ) >.
7	6	csn 3638	. 2 class { <. 0 , ( _I ` A ) >. }
8	2, 7	wceq 1373	1 wff <" A "> = { <. 0 , ( _I ` A ) >. }

This definition is referenced by:  s1val  11094  s1eq  11096  s1prc  11100