Metamath Proof Explorer

Theorem cbvsbdavw

Description: Change bound variable in proper substitution. Deduction form. (Contributed by GG, 14-Aug-2025)

Ref Expression
Hypothesis cbvsbdavw.1 ⊢ φ ∧ x = y → ψ ↔ χ
Assertion cbvsbdavw ⊢ φ → z x ψ ↔ z y χ

Proof

Step Hyp Ref Expression
1 cbvsbdavw.1 ⊢ φ ∧ x = y → ψ ↔ χ
2 equequ1 ⊢ x = y → x = t ↔ y = t
3 2 adantl ⊢ φ ∧ x = y → x = t ↔ y = t
4 3 1 imbi12d ⊢ φ ∧ x = y → x = t → ψ ↔ y = t → χ
5 4 cbvaldvaw ⊢ φ → ∀ x x = t → ψ ↔ ∀ y y = t → χ
6 5 imbi2d ⊢ φ → t = z → ∀ x x = t → ψ ↔ t = z → ∀ y y = t → χ
7 6 albidv ⊢ φ → ∀ t t = z → ∀ x x = t → ψ ↔ ∀ t t = z → ∀ y y = t → χ
8 dfsb ⊢ z x ψ ↔ ∀ t t = z → ∀ x x = t → ψ
9 dfsb ⊢ z y χ ↔ ∀ t t = z → ∀ y y = t → χ
10 7 8 9 3bitr4g ⊢ φ → z x ψ ↔ z y χ