theorem sbseq2d {x: nat} (G: wff) (a: nat x) (A B: set x):
$ G -> A == B $ >
$ G -> S[a / x] A == S[a / x] B $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hyp h | G -> A == B |
|
| 2 | 1 | eleq2d | G -> (y e. A <-> y e. B) |
| 3 | 2 | sbeq2d | G -> ([a / x] y e. A <-> [a / x] y e. B) |
| 4 | 3 | abeqd | G -> {y | [a / x] y e. A} == {y | [a / x] y e. B} |
| 5 | 4 | conv sbs | G -> S[a / x] A == S[a / x] B |