Theorem dvelimh

Version of dvelim without any variable restrictions. Usage of this theorem is discouraged because it depends on [ax-13]. Check out dvelimhw for a version requiring fewer axioms. (Contributed by NM, 1-Oct-2002.) (Proof shortened by Wolf Lammen, 11-May-2018.) (New usage is discouraged.)

Hypotheses
dvelimh.1
\( \vdash \varphi \rightarrow \forall x \, \varphi \)
dvelimh.2
\( \vdash \psi \rightarrow \forall z \, \psi \)
dvelimh.3
\( \vdash z = y \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \neg \forall x \, x = y \rightarrow \psi \rightarrow \forall x \, \psi \)
Proof
dvelimh.1
l1
nf5i _
\( \vdash \Finv x \, \varphi \)
dvelimh.2
l3
nf5i _
\( \vdash \Finv z \, \psi \)
dvelimh.3
\( \vdash z = y \rightarrow (\varphi \leftrightarrow \psi) \)
dvelimf l1 l3 _
nf5rd _