theorem app01 (a: nat): $ 0 @ a = 0 $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ndmapp | ~a e. Dom 0 -> 0 @ a = 0 |
|
| 2 | eleq2 | Dom 0 == 0 -> (a e. Dom 0 <-> a e. 0) |
|
| 3 | dm0 | Dom 0 == 0 |
|
| 4 | 2, 3 | ax_mp | a e. Dom 0 <-> a e. 0 |
| 5 | el02 | ~a e. 0 |
|
| 6 | 4, 5 | mtbir | ~a e. Dom 0 |
| 7 | 1, 6 | ax_mp | 0 @ a = 0 |