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 syl5eq 
 |-  ( ( A e. V /\ F/_ x B ) -> [_ A / x ]_ B = B )