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 | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ Ⅎ 𝑥 𝜑 ) → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝜑 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfsbcq2 | ⊢ ( 𝑦 = 𝐴 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) ) | |
2 | 1 | bibi1d | ⊢ ( 𝑦 = 𝐴 → ( ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜑 ) ↔ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝜑 ) ) ) |
3 | 2 | imbi2d | ⊢ ( 𝑦 = 𝐴 → ( ( Ⅎ 𝑥 𝜑 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜑 ) ) ↔ ( Ⅎ 𝑥 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝜑 ) ) ) ) |
4 | sbft | ⊢ ( Ⅎ 𝑥 𝜑 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜑 ) ) | |
5 | 3 4 | vtoclg | ⊢ ( 𝐴 ∈ 𝑉 → ( Ⅎ 𝑥 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝜑 ) ) ) |
6 | 5 | imp | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ Ⅎ 𝑥 𝜑 ) → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝜑 ) ) |