theorem sbsq {x: nat} (a: nat) (A: set x): $ x = a -> A == S[a / x] A $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elsbs | y e. S[a / x] A <-> [a / x] y e. A |
|
| 2 | sbq | x = a -> (y e. A <-> [a / x] y e. A) |
|
| 3 | 1, 2 | syl6bbr | x = a -> (y e. A <-> y e. S[a / x] A) |
| 4 | 3 | eqrd | x = a -> A == S[a / x] A |