theorem sabeqi {x: nat} (A B: set x): $ A == B $ > $ S\ x, A == S\ x, B $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sabeq | A. x A == B -> S\ x, A == S\ x, B |
|
2 | hyp h | A == B |
|
3 | 2 | ax_gen | A. x A == B |
4 | 1, 3 | ax_mp | S\ x, A == S\ x, B |