Theorem cbvexdva

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.)

Hypothesis
cbvaldva.1
\( \vdash \varphi \wedge x = y \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow (\exists x \, \psi \leftrightarrow \exists y \, \chi) \)
Proof
l0
nfv
l1
nfvd
cbvaldva.1
ex _
cbvexd l0 l1 _