# Metamath Proof Explorer

## Theorem cbvexdw

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

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

### Proof

Step Hyp Ref Expression
1 cbvaldw.1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
2 cbvaldw.2 ${⊢}{\phi }\to Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\psi }$
3 cbvaldw.3 ${⊢}{\phi }\to \left({x}={y}\to \left({\psi }↔{\chi }\right)\right)$
4 2 nfnd ${⊢}{\phi }\to Ⅎ{y}\phantom{\rule{.4em}{0ex}}¬{\psi }$
5 notbi ${⊢}\left({\psi }↔{\chi }\right)↔\left(¬{\psi }↔¬{\chi }\right)$
6 3 5 syl6ib ${⊢}{\phi }\to \left({x}={y}\to \left(¬{\psi }↔¬{\chi }\right)\right)$
7 1 4 6 cbvaldw ${⊢}{\phi }\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}¬{\psi }↔\forall {y}\phantom{\rule{.4em}{0ex}}¬{\chi }\right)$
8 alnex ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}¬{\psi }↔¬\exists {x}\phantom{\rule{.4em}{0ex}}{\psi }$
9 alnex ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}¬{\chi }↔¬\exists {y}\phantom{\rule{.4em}{0ex}}{\chi }$
10 7 8 9 3bitr3g ${⊢}{\phi }\to \left(¬\exists {x}\phantom{\rule{.4em}{0ex}}{\psi }↔¬\exists {y}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
11 10 con4bid ${⊢}{\phi }\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\psi }↔\exists {y}\phantom{\rule{.4em}{0ex}}{\chi }\right)$