Description: Substitution doesn't affect a constant B (in which x is not free). (Contributed by Mario Carneiro, 14-Oct-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | csbtt | |- ( ( A e. V /\ F/_ x B ) -> [_ A / x ]_ B = B ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-csb | |- [_ A / x ]_ B = { y | [. A / x ]. y e. B } |
|
2 | nfcr | |- ( F/_ x B -> F/ x y e. B ) |
|
3 | sbctt | |- ( ( A e. V /\ F/ x y e. B ) -> ( [. A / x ]. y e. B <-> y e. B ) ) |
|
4 | 2 3 | sylan2 | |- ( ( A e. V /\ F/_ x B ) -> ( [. A / x ]. y e. B <-> y e. B ) ) |
5 | 4 | abbi1dv | |- ( ( A e. V /\ F/_ x B ) -> { y | [. A / x ]. y e. B } = B ) |
6 | 1 5 | eqtrid | |- ( ( A e. V /\ F/_ x B ) -> [_ A / x ]_ B = B ) |