This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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