Definition df-s1

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 , and not, as maybe expected, the empty word, see also s1nz . (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by Mario Carneiro, 26-Feb-2016)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1	0	cs1	|- <" A ">
2		cc0	|- 0
3		cid	|- _I
4	0 3	cfv	|- ( _I ` A )
5	2 4	cop	|- <. 0 , ( _I ` A ) >.
6	5	csn	|- { <. 0 , ( _I ` A ) >. }
7	1 6	wceq	|- <" A "> = { <. 0 , ( _I ` A ) >. }