# Metamath Proof Explorer

## Theorem cbvralfw

Description: Rule used to change bound variables, using implicit substitution. Version of cbvralf with a disjoint variable condition, which does not require ax-10 , ax-13 . (Contributed by NM, 7-Mar-2004) (Revised by Gino Giotto, 23-May-2024)

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

### Proof

Step Hyp Ref Expression
1 cbvralfw.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
2 cbvralfw.2 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{A}$
3 cbvralfw.3 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
4 cbvralfw.4 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
5 cbvralfw.5 ${⊢}{x}={y}\to \left({\phi }↔{\psi }\right)$
6 2 nfcri ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{x}\in {A}$
7 6 3 nfim ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {\phi }\right)$
8 1 nfcri ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}\in {A}$
9 8 4 nfim ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\to {\psi }\right)$
10 eleq1w ${⊢}{x}={y}\to \left({x}\in {A}↔{y}\in {A}\right)$
11 10 5 imbi12d ${⊢}{x}={y}\to \left(\left({x}\in {A}\to {\phi }\right)↔\left({y}\in {A}\to {\psi }\right)\right)$
12 7 9 11 cbvalv1 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {\phi }\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\to {\psi }\right)$
13 df-ral ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {\phi }\right)$
14 df-ral ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\to {\psi }\right)$
15 12 13 14 3bitr4i ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }$