theorem sbnid {x: nat} (a: nat x): $ N[x / x] a = a $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbid | [x / x] y = a <-> y = a |
|
2 | 1 | a1i | T. -> ([x / x] y = a <-> y = a) |
3 | 2 | eqtheabd | T. -> the {y | [x / x] y = a} = a |
4 | 3 | conv sbn | T. -> N[x / x] a = a |
5 | 4 | trud | N[x / x] a = a |