theorem sbseqd (G: wff) {x: nat} (a b: nat) (A B: set x): $ G -> a = b $ > $ G -> A == B $ > $ G -> S[a / x] A == S[b / x] B $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hyp h1 | G -> a = b |
|
2 | 1 | sbseq1d | G -> S[a / x] A == S[b / x] A |
3 | hyp h2 | G -> A == B |
|
4 | 3 | sbseq2d | G -> S[b / x] A == S[b / x] B |
5 | 2, 4 | eqstrd | G -> S[a / x] A == S[b / x] B |