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

Metamath Proof Explorer

Theorem cbval2

Description: Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbval2v if possible. (Contributed by NM, 22-Dec-2003) (Revised by Mario Carneiro, 6-Oct-2016) (Proof shortened by Wolf Lammen, 11-Sep-2023) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 cbval2.1 ⊢ Ⅎ z φ
2 cbval2.2 ⊢ Ⅎ w φ
3 cbval2.3 ⊢ Ⅎ x ψ
4 cbval2.4 ⊢ Ⅎ y ψ
5 cbval2.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 cbv2 ⊢ x = z → ∀ y φ ↔ ∀ w ψ
14 6 7 13 cbval ⊢ ∀ x ∀ y φ ↔ ∀ z ∀ w ψ