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 14542
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 14550, and not, as maybe expected, the empty word, see also s1nz 14553. (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 14541 . 2 class ⟨“𝐴”⟩
3 cc0 11106 . . . 4 class 0
4 cid 5572 . . . . 5 class I
51, 4cfv 6540 . . . 4 class ( I ‘𝐴)
63, 5cop 4633 . . 3 class ⟨0, ( I ‘𝐴)⟩
76csn 4627 . 2 class {⟨0, ( I ‘𝐴)⟩}
82, 7wceq 1542 1 wff ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}
Colors of variables: wff setvar class
This definition is referenced by:  ids1  14543  s1val  14544  s1eq  14546  s1len  14552  s1nz  14553  funcnvs1  14859
  Copyright terms: Public domain W3C validator