# 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}\phantom{\rule{.4em}{0ex}}{\phi }$
cbval2.2 ${⊢}Ⅎ{w}\phantom{\rule{.4em}{0ex}}{\phi }$
cbval2.3 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
cbval2.4 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\psi }$
cbval2.5 ${⊢}\left({x}={z}\wedge {y}={w}\right)\to \left({\phi }↔{\psi }\right)$
Assertion cbval2 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {z}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}{\psi }$

### Proof

Step Hyp Ref Expression
1 cbval2.1 ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}{\phi }$
2 cbval2.2 ${⊢}Ⅎ{w}\phantom{\rule{.4em}{0ex}}{\phi }$
3 cbval2.3 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
4 cbval2.4 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\psi }$
5 cbval2.5 ${⊢}\left({x}={z}\wedge {y}={w}\right)\to \left({\phi }↔{\psi }\right)$
6 1 nfal ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }$
7 3 nfal ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}{\psi }$
8 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{x}={z}$
9 nfv ${⊢}Ⅎ{w}\phantom{\rule{.4em}{0ex}}{x}={z}$
10 2 a1i ${⊢}{x}={z}\to Ⅎ{w}\phantom{\rule{.4em}{0ex}}{\phi }$
11 4 a1i ${⊢}{x}={z}\to Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\psi }$
12 5 ex ${⊢}{x}={z}\to \left({y}={w}\to \left({\phi }↔{\psi }\right)\right)$
13 8 9 10 11 12 cbv2 ${⊢}{x}={z}\to \left(\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {w}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
14 6 7 13 cbval ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {z}\phantom{\rule{.4em}{0ex}}\forall {w}\phantom{\rule{.4em}{0ex}}{\psi }$