Theorem dvelimf

Version of dvelimv without any variable restrictions. Usage of this theorem is discouraged because it depends on [ax-13]. (Contributed by NM, 1-Oct-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 11-May-2018.) (New usage is discouraged.)

Hypotheses
dvelimf.1
\( \vdash \Finv x \, \varphi \)
dvelimf.2
\( \vdash \Finv z \, \psi \)
dvelimf.3
\( \vdash z = y \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \neg \forall x \, x = y \rightarrow \Finv x \, \psi \)
Proof
l0
dvelimf.2
dvelimf.3
equsal l0 _
l3
bicomi _
\( \vdash \psi \leftrightarrow \forall z \, (z = y \rightarrow \varphi) \)
l4
nfnae
nfeqf
l6
ancoms _
dvelimf.1
a1i _
nfimd l6 _
nfald2 l4 _
\( \vdash \neg \forall x \, x = y \rightarrow \Finv x \, \forall z \, (z = y \rightarrow \varphi) \)
nfxfrd l3 _