![]() |
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 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.) |
Ref | Expression |
---|---|
df-s1 | ⊢ 〈“𝐴”〉 = {〈0, ( I ‘𝐴)〉} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | 1 | cs1 14541 | . 2 class 〈“𝐴”〉 |
3 | cc0 11106 | . . . 4 class 0 | |
4 | cid 5572 | . . . . 5 class I | |
5 | 1, 4 | cfv 6540 | . . . 4 class ( I ‘𝐴) |
6 | 3, 5 | cop 4633 | . . 3 class 〈0, ( I ‘𝐴)〉 |
7 | 6 | csn 4627 | . 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 14543 s1val 14544 s1eq 14546 s1len 14552 s1nz 14553 funcnvs1 14859 |
Copyright terms: Public domain | W3C validator |