Metamath Proof Explorer


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 ) >. }