# Metamath Proof Explorer

## Theorem cbvralsvw

Description: Change bound variable by using a substitution. Version of cbvralsv with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 20-Nov-2005) (Revised by Gino Giotto, 10-Jan-2024)

Ref Expression
Assertion cbvralsvw ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left[{y}/{x}\right]{\phi }$

### Proof

Step Hyp Ref Expression
1 nfv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}{\phi }$
2 nfs1v ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left[{z}/{x}\right]{\phi }$
3 sbequ12 ${⊢}{x}={z}\to \left({\phi }↔\left[{z}/{x}\right]{\phi }\right)$
4 1 2 3 cbvralw ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left[{z}/{x}\right]{\phi }$
5 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left[{z}/{x}\right]{\phi }$
6 nfv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left[{y}/{x}\right]{\phi }$
7 sbequ ${⊢}{z}={y}\to \left(\left[{z}/{x}\right]{\phi }↔\left[{y}/{x}\right]{\phi }\right)$
8 5 6 7 cbvralw ${⊢}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\left[{z}/{x}\right]{\phi }↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left[{y}/{x}\right]{\phi }$
9 4 8 bitri ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left[{y}/{x}\right]{\phi }$