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 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.) |
Ref | Expression |
---|---|
df-s1 | ⊢ 〈“𝐴”〉 = {〈0, ( I ‘𝐴)〉} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | 1 | cs1 13939 | . 2 class 〈“𝐴”〉 |
3 | cc0 10526 | . . . 4 class 0 | |
4 | cid 5453 | . . . . 5 class I | |
5 | 1, 4 | cfv 6349 | . . . 4 class ( I ‘𝐴) |
6 | 3, 5 | cop 4565 | . . 3 class 〈0, ( I ‘𝐴)〉 |
7 | 6 | csn 4559 | . 2 class {〈0, ( I ‘𝐴)〉} |
8 | 2, 7 | wceq 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 |