# Metamath Proof Explorer

## Theorem cbvrabw

Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. Version of cbvrab with a disjoint variable condition, which does not require ax-13 . (Contributed by Andrew Salmon, 11-Jul-2011) (Revised by Gino Giotto, 10-Jan-2024)

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

### Proof

Step Hyp Ref Expression
1 cbvrabw.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
2 cbvrabw.2 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{A}$
3 cbvrabw.3 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
4 cbvrabw.4 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
5 cbvrabw.5 ${⊢}{x}={y}\to \left({\phi }↔{\psi }\right)$
6 nfv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\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 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({z}\in {A}\wedge \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 anbi12d ${⊢}{x}={z}\to \left(\left({x}\in {A}\wedge {\phi }\right)↔\left({z}\in {A}\wedge \left[{z}/{x}\right]{\phi }\right)\right)$
13 6 9 12 cbvabw ${⊢}\left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}=\left\{{z}|\left({z}\in {A}\wedge \left[{z}/{x}\right]{\phi }\right)\right\}$
14 2 nfcri ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{z}\in {A}$
15 3 nfsbv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left[{z}/{x}\right]{\phi }$
16 14 15 nfan ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left({z}\in {A}\wedge \left[{z}/{x}\right]{\phi }\right)$
17 nfv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\wedge {\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 sbiev ${⊢}\left[{y}/{x}\right]{\phi }↔{\psi }$
21 19 20 syl6bb ${⊢}{z}={y}\to \left(\left[{z}/{x}\right]{\phi }↔{\psi }\right)$
22 18 21 anbi12d ${⊢}{z}={y}\to \left(\left({z}\in {A}\wedge \left[{z}/{x}\right]{\phi }\right)↔\left({y}\in {A}\wedge {\psi }\right)\right)$
23 16 17 22 cbvabw ${⊢}\left\{{z}|\left({z}\in {A}\wedge \left[{z}/{x}\right]{\phi }\right)\right\}=\left\{{y}|\left({y}\in {A}\wedge {\psi }\right)\right\}$
24 13 23 eqtri ${⊢}\left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}=\left\{{y}|\left({y}\in {A}\wedge {\psi }\right)\right\}$
25 df-rab ${⊢}\left\{{x}\in {A}|{\phi }\right\}=\left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}$
26 df-rab ${⊢}\left\{{y}\in {A}|{\psi }\right\}=\left\{{y}|\left({y}\in {A}\wedge {\psi }\right)\right\}$
27 24 25 26 3eqtr4i ${⊢}\left\{{x}\in {A}|{\phi }\right\}=\left\{{y}\in {A}|{\psi }\right\}$