Theorem cbvexdvaw

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.) Avoid [ax-13]. (Revised by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by Wolf Lammen, 10-Feb-2024.)

Hypothesis
cbvaldvaw.1
\( \vdash \varphi \wedge x = y \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow (\exists x \, \psi \leftrightarrow \exists y \, \chi) \)
Proof
cbvaldvaw.1
notbid _
l2
cbvaldvaw _
\( \vdash \varphi \rightarrow (\forall x \, \neg \psi \leftrightarrow \forall y \, \neg \chi) \)
l3
alnex
\( \vdash \forall x \, \neg \psi \leftrightarrow \neg \exists x \, \psi \)
alnex
\( \vdash \forall y \, \neg \chi \leftrightarrow \neg \exists y \, \chi \)
3bitr3g l2 l3 _
con4bid _