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

Metamath Proof Explorer

Theorem cbval2v

Description: Rule used to change bound variables, using implicit substitution. Version of cbval2 with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 22-Dec-2003) (Revised by BJ, 16-Jun-2019) (Proof shortened by GG, 10-Jan-2024)

Ref Expression
Hypotheses cbval2v.1 ⊢ Ⅎ z φ
cbval2v.2 ⊢ Ⅎ w φ
cbval2v.3 ⊢ Ⅎ x ψ
cbval2v.4 ⊢ Ⅎ y ψ
cbval2v.5 ⊢ x = z ∧ y = w → φ ↔ ψ
Assertion cbval2v ⊢ ∀ x ∀ y φ ↔ ∀ z ∀ w ψ

Proof

Step Hyp Ref Expression
1 cbval2v.1 ⊢ Ⅎ z φ
2 cbval2v.2 ⊢ Ⅎ w φ
3 cbval2v.3 ⊢ Ⅎ x ψ
4 cbval2v.4 ⊢ Ⅎ y ψ
5 cbval2v.5 ⊢ x = z ∧ y = w → φ ↔ ψ
6 1 nfal ⊢ Ⅎ z ∀ y φ
7 3 nfal ⊢ Ⅎ x ∀ w ψ
8 nfv ⊢ Ⅎ y x = z
9 nfv ⊢ Ⅎ w x = z
10 2 a1i ⊢ x = z → Ⅎ w φ
11 4 a1i ⊢ x = z → Ⅎ y ψ
12 5 ex ⊢ x = z → y = w → φ ↔ ψ
13 8 9 10 11 12 cbv2w ⊢ x = z → ∀ y φ ↔ ∀ w ψ
14 6 7 13 cbvalv1 ⊢ ∀ x ∀ y φ ↔ ∀ z ∀ w ψ