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”⟩=\left\{⟨0,\mathrm{I}\left(A\right)⟩\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1	0	cs1	$$class⟨“A”⟩$$
2		cc0	$$class0$$
3		cid	$$class\mathrm{I}$$
4	0 3	cfv	$$class\mathrm{I}\left(A\right)$$
5	2 4	cop	$$class⟨0,\mathrm{I}\left(A\right)⟩$$
6	5	csn	$$class\left\{⟨0,\mathrm{I}\left(A\right)⟩\right\}$$
7	1 6	wceq	$$wff⟨“A”⟩=\left\{⟨0,\mathrm{I}\left(A\right)⟩\right\}$$