![]() |
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 14638, and not, as maybe expected, the empty word, see also s1nz 14641. (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 14629 | . 2 class 〈“𝐴”〉 |
3 | cc0 11152 | . . . 4 class 0 | |
4 | cid 5581 | . . . . 5 class I | |
5 | 1, 4 | cfv 6562 | . . . 4 class ( I ‘𝐴) |
6 | 3, 5 | cop 4636 | . . 3 class 〈0, ( I ‘𝐴)〉 |
7 | 6 | csn 4630 | . 2 class {〈0, ( I ‘𝐴)〉} |
8 | 2, 7 | wceq 1536 | 1 wff 〈“𝐴”〉 = {〈0, ( I ‘𝐴)〉} |
Colors of variables: wff setvar class |
This definition is referenced by: ids1 14631 s1val 14632 s1eq 14634 s1len 14640 s1nz 14641 funcnvs1 14947 |
Copyright terms: Public domain | W3C validator |