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 13940
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 13948, and not, as maybe expected, the empty word, see also s1nz 13951. (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 13939 . 2 class ⟨“𝐴”⟩
3 cc0 10526 . . . 4 class 0
4 cid 5453 . . . . 5 class I
51, 4cfv 6349 . . . 4 class ( I ‘𝐴)
63, 5cop 4565 . . 3 class ⟨0, ( I ‘𝐴)⟩
76csn 4559 . 2 class {⟨0, ( I ‘𝐴)⟩}
82, 7wceq 1528 1 wff ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}
Colors of variables: wff setvar class
This definition is referenced by:  ids1  13941  s1val  13942  s1eq  13944  s1len  13950  s1nz  13951  funcnvs1  14264
  Copyright terms: Public domain W3C validator