# Metamath Proof Explorer

## Theorem cbvrexsvw

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

Ref Expression
Assertion cbvrexsvw ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {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 cbvrexw ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {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 cbvrexw ${⊢}\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}\left[{z}/{x}\right]{\phi }↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\left[{y}/{x}\right]{\phi }$
9 4 8 bitri ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\left[{y}/{x}\right]{\phi }$