![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-s1 | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
df-s1 | ⊢ ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | 1 | cs1 14545 | . 2 class ⟨“𝐴”⟩ |
3 | cc0 11110 | . . . 4 class 0 | |
4 | cid 5574 | . . . . 5 class I | |
5 | 1, 4 | cfv 6544 | . . . 4 class ( I ‘𝐴) |
6 | 3, 5 | cop 4635 | . . 3 class ⟨0, ( I ‘𝐴)⟩ |
7 | 6 | csn 4629 | . 2 class {⟨0, ( I ‘𝐴)⟩} |
8 | 2, 7 | wceq 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 |