| 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 14642, and not, as maybe expected, the empty word, see also s1nz 14645. (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 14633 | . 2 class 〈“𝐴”〉 |
| 3 | cc0 11155 | . . . 4 class 0 | |
| 4 | cid 5577 | . . . . 5 class I | |
| 5 | 1, 4 | cfv 6561 | . . . 4 class ( I ‘𝐴) |
| 6 | 3, 5 | cop 4632 | . . 3 class 〈0, ( I ‘𝐴)〉 |
| 7 | 6 | csn 4626 | . 2 class {〈0, ( I ‘𝐴)〉} |
| 8 | 2, 7 | wceq 1540 | 1 wff 〈“𝐴”〉 = {〈0, ( I ‘𝐴)〉} |
| Colors of variables: wff setvar class |
| This definition is referenced by: ids1 14635 s1val 14636 s1eq 14638 s1len 14644 s1nz 14645 funcnvs1 14951 |
| Copyright terms: Public domain | W3C validator |