Metamath Proof Explorer


Theorem sbctt

Description: Substitution for a variable not free in a wff does not affect it. (Contributed by Mario Carneiro, 14-Oct-2016)

Ref Expression
Assertion sbctt
|- ( ( A e. V /\ F/ x ph ) -> ( [. A / x ]. ph <-> ph ) )

Proof

Step Hyp Ref Expression
1 dfsbcq2
 |-  ( y = A -> ( [ y / x ] ph <-> [. A / x ]. ph ) )
2 1 bibi1d
 |-  ( y = A -> ( ( [ y / x ] ph <-> ph ) <-> ( [. A / x ]. ph <-> ph ) ) )
3 2 imbi2d
 |-  ( y = A -> ( ( F/ x ph -> ( [ y / x ] ph <-> ph ) ) <-> ( F/ x ph -> ( [. A / x ]. ph <-> ph ) ) ) )
4 sbft
 |-  ( F/ x ph -> ( [ y / x ] ph <-> ph ) )
5 3 4 vtoclg
 |-  ( A e. V -> ( F/ x ph -> ( [. A / x ]. ph <-> ph ) ) )
6 5 imp
 |-  ( ( A e. V /\ F/ x ph ) -> ( [. A / x ]. ph <-> ph ) )