# Metamath Proof Explorer

## Theorem cbv1v

Description: Rule used to change bound variables, using implicit substitution. Version of cbv1 with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 5-Aug-1993) (Revised by BJ, 16-Jun-2019)

Ref Expression
Hypotheses cbv1v.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
cbv1v.2 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
cbv1v.3 ${⊢}{\phi }\to Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\psi }$
cbv1v.4 ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\chi }$
cbv1v.5 ${⊢}{\phi }\to \left({x}={y}\to \left({\psi }\to {\chi }\right)\right)$
Assertion cbv1v ${⊢}{\phi }\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\to \forall {y}\phantom{\rule{.4em}{0ex}}{\chi }\right)$

### Proof

Step Hyp Ref Expression
1 cbv1v.1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 cbv1v.2 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
3 cbv1v.3 ${⊢}{\phi }\to Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\psi }$
4 cbv1v.4 ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\chi }$
5 cbv1v.5 ${⊢}{\phi }\to \left({x}={y}\to \left({\psi }\to {\chi }\right)\right)$
6 2 3 nfim1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)$
7 1 4 nfim1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\chi }\right)$
8 5 com12 ${⊢}{x}={y}\to \left({\phi }\to \left({\psi }\to {\chi }\right)\right)$
9 8 a2d ${⊢}{x}={y}\to \left(\left({\phi }\to {\psi }\right)\to \left({\phi }\to {\chi }\right)\right)$
10 6 7 9 cbv3v ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)\to \forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\chi }\right)$
11 1 19.21 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\psi }\right)↔\left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
12 2 19.21 ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {\chi }\right)↔\left({\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
13 10 11 12 3imtr3i ${⊢}\left({\phi }\to \forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)\to \left({\phi }\to \forall {y}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
14 13 pm2.86i ${⊢}{\phi }\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{\psi }\to \forall {y}\phantom{\rule{.4em}{0ex}}{\chi }\right)$