# Metamath Proof Explorer

## Theorem cbvexd

Description: Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim . Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvexdw if possible. (Contributed by NM, 2-Jan-2002) (Revised by Mario Carneiro, 6-Oct-2016) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 cbvald.1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
2 cbvald.2 ${⊢}{\phi }\to Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\psi }$
3 cbvald.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 cbvald ${⊢}{\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)$