# Metamath Proof Explorer

## Theorem cbvrexsv

Description: Change bound variable by using a substitution. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvrexsvw when possible. (Contributed by NM, 2-Mar-2008) (Revised by Andrew Salmon, 11-Jul-2011) (New usage is discouraged.)

Ref Expression
Assertion cbvrexsv ${⊢}\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 cbvrex ${⊢}\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}}{\phi }$
6 5 nfsb ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left[{z}/{x}\right]{\phi }$
7 nfv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left[{y}/{x}\right]{\phi }$
8 sbequ ${⊢}{z}={y}\to \left(\left[{z}/{x}\right]{\phi }↔\left[{y}/{x}\right]{\phi }\right)$
9 6 7 8 cbvrex ${⊢}\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 }$
10 4 9 bitri ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}\left[{y}/{x}\right]{\phi }$