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