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 13459
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 13545, and not, as maybe expected, the empty word, see also s1nz 13548. (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 13451 . 2 class ⟨“𝐴”⟩
3 cc0 10099 . . . 4 class 0
4 cid 5161 . . . . 5 class I
51, 4cfv 6037 . . . 4 class ( I ‘𝐴)
63, 5cop 4315 . . 3 class ⟨0, ( I ‘𝐴)⟩
76csn 4309 . 2 class {⟨0, ( I ‘𝐴)⟩}
82, 7wceq 1620 1 wff ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}
Colors of variables: wff setvar class
This definition is referenced by:  ids1  13538  s1val  13539  s1eq  13541  s1len  13547  s1nz  13548  funcnvs1  13828
  Copyright terms: Public domain W3C validator