# Metamath Proof Explorer

## Theorem cbvrexw

Description: Rule used to change bound variables, using implicit substitution. Version of cbvrex with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 31-Jul-2003) (Revised by Gino Giotto, 10-Jan-2024)

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

### Proof

Step Hyp Ref Expression
1 cbvralw.1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
2 cbvralw.2 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
3 cbvralw.3 ${⊢}{x}={y}\to \left({\phi }↔{\psi }\right)$
4 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
5 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{A}$
6 4 5 1 2 3 cbvrexfw ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }$