# Metamath Proof Explorer

## Theorem cbvabw

Description: Rule used to change bound variables, using implicit substitution. Version of cbvab with a disjoint variable condition, which does not require ax-10 , ax-13 . (Contributed by Andrew Salmon, 11-Jul-2011) (Revised by Gino Giotto, 23-May-2024)

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

### Proof

Step Hyp Ref Expression
1 cbvabw.1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
2 cbvabw.2 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
3 cbvabw.3 ${⊢}{x}={y}\to \left({\phi }↔{\psi }\right)$
4 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{x}={w}$
5 4 1 nfim ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left({x}={w}\to {\phi }\right)$
6 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}={w}$
7 6 2 nfim ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({y}={w}\to {\psi }\right)$
8 equequ1 ${⊢}{x}={y}\to \left({x}={w}↔{y}={w}\right)$
9 8 3 imbi12d ${⊢}{x}={y}\to \left(\left({x}={w}\to {\phi }\right)↔\left({y}={w}\to {\psi }\right)\right)$
10 5 7 9 cbvalv1 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={w}\to {\phi }\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}={w}\to {\psi }\right)$
11 10 imbi2i ${⊢}\left({w}={z}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={w}\to {\phi }\right)\right)↔\left({w}={z}\to \forall {y}\phantom{\rule{.4em}{0ex}}\left({y}={w}\to {\psi }\right)\right)$
12 11 albii ${⊢}\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}={z}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={w}\to {\phi }\right)\right)↔\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}={z}\to \forall {y}\phantom{\rule{.4em}{0ex}}\left({y}={w}\to {\psi }\right)\right)$
13 df-sb ${⊢}\left[{z}/{x}\right]{\phi }↔\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}={z}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={w}\to {\phi }\right)\right)$
14 df-sb ${⊢}\left[{z}/{y}\right]{\psi }↔\forall {w}\phantom{\rule{.4em}{0ex}}\left({w}={z}\to \forall {y}\phantom{\rule{.4em}{0ex}}\left({y}={w}\to {\psi }\right)\right)$
15 12 13 14 3bitr4i ${⊢}\left[{z}/{x}\right]{\phi }↔\left[{z}/{y}\right]{\psi }$
16 df-clab ${⊢}{z}\in \left\{{x}|{\phi }\right\}↔\left[{z}/{x}\right]{\phi }$
17 df-clab ${⊢}{z}\in \left\{{y}|{\psi }\right\}↔\left[{z}/{y}\right]{\psi }$
18 15 16 17 3bitr4i ${⊢}{z}\in \left\{{x}|{\phi }\right\}↔{z}\in \left\{{y}|{\psi }\right\}$
19 18 eqriv ${⊢}\left\{{x}|{\phi }\right\}=\left\{{y}|{\psi }\right\}$