theorem sbseh {x: nat} (a: nat) (A B: set x):
$ FS/ x B $ >
$ x = a -> A == B $ >
$ S[a / x] A == B $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hyp h | FS/ x B |
|
| 2 | 1 | sbseht | A. x (x = a -> A == B) -> S[a / x] A == B |
| 3 | hyp e | x = a -> A == B |
|
| 4 | 3 | ax_gen | A. x (x = a -> A == B) |
| 5 | 2, 4 | ax_mp | S[a / x] A == B |