Metamath Proof Explorer

Theorem cbvsbdavw2

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

Ref Expression
Hypotheses cbvsbdavw2.1 ⊢ φ → z = w
cbvsbdavw2.2 ⊢ φ ∧ x = y → ψ ↔ χ
Assertion cbvsbdavw2 ⊢ φ → z x ψ ↔ w y χ

Proof

Step Hyp Ref Expression
1 cbvsbdavw2.1 ⊢ φ → z = w
2 cbvsbdavw2.2 ⊢ φ ∧ x = y → ψ ↔ χ
3 equequ2 ⊢ z = w → t = z ↔ t = w
4 1 3 syl ⊢ φ → t = z ↔ t = w
5 equequ1 ⊢ x = y → x = t ↔ y = t
6 5 adantl ⊢ φ ∧ x = y → x = t ↔ y = t
7 6 2 imbi12d ⊢ φ ∧ x = y → x = t → ψ ↔ y = t → χ
8 7 cbvaldvaw ⊢ φ → ∀ x x = t → ψ ↔ ∀ y y = t → χ
9 4 8 imbi12d ⊢ φ → t = z → ∀ x x = t → ψ ↔ t = w → ∀ y y = t → χ
10 9 albidv ⊢ φ → ∀ t t = z → ∀ x x = t → ψ ↔ ∀ t t = w → ∀ y y = t → χ
11 df-sb ⊢ z x ψ ↔ ∀ t t = z → ∀ x x = t → ψ
12 df-sb ⊢ w y χ ↔ ∀ t t = w → ∀ y y = t → χ
13 10 11 12 3bitr4g ⊢ φ → z x ψ ↔ w y χ