MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-s1 Structured version   Visualization version   GIF version

Definition df-s1 13334
Description: Define the canonical injection from symbols to words. Although not required, 𝐴 should usually be a set. Otherwise, the singleton word ⟨“𝐴”⟩ would be the singleton word consisting of the empty set, see s1prc 13420, and not, as maybe expected, the empty word, see also s1nz 13423. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
Assertion
Ref Expression
df-s1 ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}

Detailed syntax breakdown of Definition df-s1
StepHypRef Expression
1 cA . . 3 class 𝐴
21cs1 13326 . 2 class ⟨“𝐴”⟩
3 cc0 9974 . . . 4 class 0
4 cid 5052 . . . . 5 class I
51, 4cfv 5926 . . . 4 class ( I ‘𝐴)
63, 5cop 4216 . . 3 class ⟨0, ( I ‘𝐴)⟩
76csn 4210 . 2 class {⟨0, ( I ‘𝐴)⟩}
82, 7wceq 1523 1 wff ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}
Colors of variables: wff setvar class
This definition is referenced by:  ids1  13413  s1val  13414  s1eq  13416  s1len  13422  s1nz  13423  funcnvs1  13703
  Copyright terms: Public domain W3C validator