theorem sbneh {x: nat} (a: nat) (b c: nat x): $ FN/ x c $ > $ x = a -> b = c $ > $ N[a / x] b = c $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hyp h | FN/ x c |
|
2 | 1 | sbneht | A. x (x = a -> b = c) -> N[a / x] b = c |
3 | hyp e | x = a -> b = c |
|
4 | 3 | ax_gen | A. x (x = a -> b = c) |
5 | 2, 4 | ax_mp | N[a / x] b = c |