# Metamath Proof Explorer

## Theorem cbvexdva

Description: Rule used to change the bound variable in an existential quantifier with implicit substitution. Deduction form. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvexdvaw if possible. (Contributed by David Moews, 1-May-2017) (New usage is discouraged.)

Ref Expression
Hypothesis cbvaldva.1 ${⊢}\left({\phi }\wedge {x}={y}\right)\to \left({\psi }↔{\chi }\right)$
Assertion cbvexdva ${⊢}{\phi }\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\psi }↔\exists {y}\phantom{\rule{.4em}{0ex}}{\chi }\right)$

### Proof

Step Hyp Ref Expression
1 cbvaldva.1 ${⊢}\left({\phi }\wedge {x}={y}\right)\to \left({\psi }↔{\chi }\right)$
2 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
3 nfvd ${⊢}{\phi }\to Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\psi }$
4 1 ex ${⊢}{\phi }\to \left({x}={y}\to \left({\psi }↔{\chi }\right)\right)$
5 2 3 4 cbvexd ${⊢}{\phi }\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\psi }↔\exists {y}\phantom{\rule{.4em}{0ex}}{\chi }\right)$