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