theorem sbnq {x: nat} (a: nat) (b: nat x): $ x = a -> b = N[a / x] b $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sbq | x = a -> (y = b <-> [a / x] y = b) |
|
| 2 | 1 | bicomd | x = a -> ([a / x] y = b <-> y = b) |
| 3 | 2 | eqtheabd | x = a -> the {y | [a / x] y = b} = b |
| 4 | 3 | conv sbn | x = a -> N[a / x] b = b |
| 5 | 4 | eqcomd | x = a -> b = N[a / x] b |