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 14546
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 14554, and not, as maybe expected, the empty word, see also s1nz 14557. (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 14545 . 2 class ⟨“𝐴”⟩
3 cc0 11110 . . . 4 class 0
4 cid 5574 . . . . 5 class I
51, 4cfv 6544 . . . 4 class ( I ‘𝐴)
63, 5cop 4635 . . 3 class ⟨0, ( I ‘𝐴)⟩
76csn 4629 . 2 class {⟨0, ( I ‘𝐴)⟩}
82, 7wceq 1542 1 wff ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}
Colors of variables: wff setvar class
This definition is referenced by:  ids1  14547  s1val  14548  s1eq  14550  s1len  14556  s1nz  14557  funcnvs1  14863
  Copyright terms: Public domain W3C validator