# Metamath Proof Explorer

## Theorem cbvexdvaw

Description: Rule used to change the bound variable in an existential quantifier with implicit substitution. Deduction form. Version of cbvexdva with a disjoint variable condition, requiring fewer axioms. (Contributed by David Moews, 1-May-2017) (Revised by Gino Giotto, 10-Jan-2024) Reduce axiom usage. (Revised by Wolf Lammen, 10-Feb-2024)

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

### Proof

Step Hyp Ref Expression
1 cbvaldvaw.1 ${⊢}\left({\phi }\wedge {x}={y}\right)\to \left({\psi }↔{\chi }\right)$
2 1 notbid ${⊢}\left({\phi }\wedge {x}={y}\right)\to \left(¬{\psi }↔¬{\chi }\right)$
3 2 cbvaldvaw ${⊢}{\phi }\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}¬{\psi }↔\forall {y}\phantom{\rule{.4em}{0ex}}¬{\chi }\right)$
4 alnex ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}¬{\psi }↔¬\exists {x}\phantom{\rule{.4em}{0ex}}{\psi }$
5 alnex ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}¬{\chi }↔¬\exists {y}\phantom{\rule{.4em}{0ex}}{\chi }$
6 3 4 5 3bitr3g ${⊢}{\phi }\to \left(¬\exists {x}\phantom{\rule{.4em}{0ex}}{\psi }↔¬\exists {y}\phantom{\rule{.4em}{0ex}}{\chi }\right)$
7 6 con4bid ${⊢}{\phi }\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\psi }↔\exists {y}\phantom{\rule{.4em}{0ex}}{\chi }\right)$