This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ V ∧ Ⅎ x φ → [˙A / x]˙ φ ↔ φ

Proof

Step Hyp Ref Expression
1 dfsbcq2 ⊢ y = A → y x φ ↔ [˙A / x]˙ φ
2 1 bibi1d ⊢ y = A → y x φ ↔ φ ↔ [˙A / x]˙ φ ↔ φ
3 2 imbi2d ⊢ y = A → Ⅎ x φ → y x φ ↔ φ ↔ Ⅎ x φ → [˙A / x]˙ φ ↔ φ
4 sbft ⊢ Ⅎ x φ → y x φ ↔ φ
5 3 4 vtoclg ⊢ A ∈ V → Ⅎ x φ → [˙A / x]˙ φ ↔ φ
6 5 imp ⊢ A ∈ V ∧ Ⅎ x φ → [˙A / x]˙ φ ↔ φ