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 ) ) |
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 ) ) |