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

Metamath Proof Explorer

Theorem cbvsbvf

Description: Change the bound variable (i.e. the substituted one) in wff's linked by implicit substitution. The proof was part of a former cbvabw version. (Contributed by GG and WL, 26-Oct-2024)

Ref Expression
Hypotheses cbvsbvf.1 ⊢ Ⅎ y φ
cbvsbvf.2 ⊢ Ⅎ x ψ
cbvsbvf.3 ⊢ x = y → φ ↔ ψ
Assertion cbvsbvf ⊢ z x φ ↔ z y ψ

Proof

Step Hyp Ref Expression
1 cbvsbvf.1 ⊢ Ⅎ y φ
2 cbvsbvf.2 ⊢ Ⅎ x ψ
3 cbvsbvf.3 ⊢ x = y → φ ↔ ψ
4 nfv ⊢ Ⅎ y x = w
5 4 1 nfim ⊢ Ⅎ y x = w → φ
6 nfv ⊢ Ⅎ x y = w
7 6 2 nfim ⊢ Ⅎ x y = w → ψ
8 equequ1 ⊢ x = y → x = w ↔ y = w
9 8 3 imbi12d ⊢ x = y → x = w → φ ↔ y = w → ψ
10 5 7 9 cbvalv1 ⊢ ∀ x x = w → φ ↔ ∀ y y = w → ψ
11 10 imbi2i ⊢ w = z → ∀ x x = w → φ ↔ w = z → ∀ y y = w → ψ
12 11 albii ⊢ ∀ w w = z → ∀ x x = w → φ ↔ ∀ w w = z → ∀ y y = w → ψ
13 dfsb ⊢ z x φ ↔ ∀ w w = z → ∀ x x = w → φ
14 dfsb ⊢ z y ψ ↔ ∀ w w = z → ∀ y y = w → ψ
15 12 13 14 3bitr4i ⊢ z x φ ↔ z y ψ