Theorem dvelimv

Similar to dvelim with first hypothesis replaced by a distinct variable condition. Usage of this theorem is discouraged because it depends on [ax-13]. Check out dvelimhw for a version requiring fewer axioms. (Contributed by NM, 25-Jul-2015.) (Proof shortened by Wolf Lammen, 30-Apr-2018.) (New usage is discouraged.)

Hypothesis
dvelimv.1
\( \vdash z = y \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \neg \forall x \, x = y \rightarrow \psi \rightarrow \forall x \, \psi \)
Proof
l0
ax-5
\( \vdash \varphi \rightarrow \forall x \, \varphi \)
dvelimv.1
\( \vdash z = y \rightarrow (\varphi \leftrightarrow \psi) \)
dvelim l0 _