# Metamath Proof Explorer

## Theorem cbvralf

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 cbvralfw when possible. (Contributed by NM, 7-Mar-2004) (Revised by Mario Carneiro, 9-Oct-2016) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 cbvralf.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
2 cbvralf.2 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{A}$
3 cbvralf.3 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
4 cbvralf.4 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
5 cbvralf.5 ${⊢}{x}={y}\to \left({\phi }↔{\psi }\right)$
6 nfv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {\phi }\right)$
7 1 nfcri ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{z}\in {A}$
8 nfs1v ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left[{z}/{x}\right]{\phi }$
9 7 8 nfim ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({z}\in {A}\to \left[{z}/{x}\right]{\phi }\right)$
10 eleq1w ${⊢}{x}={z}\to \left({x}\in {A}↔{z}\in {A}\right)$
11 sbequ12 ${⊢}{x}={z}\to \left({\phi }↔\left[{z}/{x}\right]{\phi }\right)$
12 10 11 imbi12d ${⊢}{x}={z}\to \left(\left({x}\in {A}\to {\phi }\right)↔\left({z}\in {A}\to \left[{z}/{x}\right]{\phi }\right)\right)$
13 6 9 12 cbvalv1 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {\phi }\right)↔\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {A}\to \left[{z}/{x}\right]{\phi }\right)$
14 2 nfcri ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{z}\in {A}$
15 3 nfsb ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left[{z}/{x}\right]{\phi }$
16 14 15 nfim ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left({z}\in {A}\to \left[{z}/{x}\right]{\phi }\right)$
17 nfv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\to {\psi }\right)$
18 eleq1w ${⊢}{z}={y}\to \left({z}\in {A}↔{y}\in {A}\right)$
19 sbequ ${⊢}{z}={y}\to \left(\left[{z}/{x}\right]{\phi }↔\left[{y}/{x}\right]{\phi }\right)$
20 4 5 sbie ${⊢}\left[{y}/{x}\right]{\phi }↔{\psi }$
21 19 20 syl6bb ${⊢}{z}={y}\to \left(\left[{z}/{x}\right]{\phi }↔{\psi }\right)$
22 18 21 imbi12d ${⊢}{z}={y}\to \left(\left({z}\in {A}\to \left[{z}/{x}\right]{\phi }\right)↔\left({y}\in {A}\to {\psi }\right)\right)$
23 16 17 22 cbvalv1 ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {A}\to \left[{z}/{x}\right]{\phi }\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\to {\psi }\right)$
24 13 23 bitri ${⊢}\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)$
25 df-ral ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {\phi }\right)$
26 df-ral ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\to {\psi }\right)$
27 24 25 26 3bitr4i ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }$