# Metamath Proof Explorer

## Theorem cbvrexfw

Description: Rule used to change bound variables, using implicit substitution. Version of cbvrexf with a disjoint variable condition, which does not require ax-13 . (Contributed by FL, 27-Apr-2008) (Revised by Gino Giotto, 10-Jan-2024)

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

### Proof

Step Hyp Ref Expression
1 cbvrexfw.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
2 cbvrexfw.2 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{A}$
3 cbvrexfw.3 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
4 cbvrexfw.4 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
5 cbvrexfw.5 ${⊢}{x}={y}\to \left({\phi }↔{\psi }\right)$
6 3 nfn ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}¬{\phi }$
7 4 nfn ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}¬{\psi }$
8 5 notbid ${⊢}{x}={y}\to \left(¬{\phi }↔¬{\psi }\right)$
9 1 2 6 7 8 cbvralfw ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{\phi }↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{\psi }$
10 9 notbii ${⊢}¬\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{\phi }↔¬\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{\psi }$
11 dfrex2 ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔¬\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{\phi }$
12 dfrex2 ${⊢}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }↔¬\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{\psi }$
13 10 11 12 3bitr4i ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }$