Metamath Proof Explorer


Theorem csbtt

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 )

Proof

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 )