# Metamath Proof Explorer

## Theorem cbvralsv

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

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