Theorem dvelimnf

Version of dvelim using "not free" notation. Usage of this theorem is discouraged because it depends on [ax-13]. (Contributed by Mario Carneiro, 9-Oct-2016.) (New usage is discouraged.)

Hypotheses
dvelimnf.1
\( \vdash \Finv x \, \varphi \)
dvelimnf.2
\( \vdash z = y \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \neg \forall x \, x = y \rightarrow \Finv x \, \psi \)
Proof
l0
dvelimnf.1
\( \vdash \Finv x \, \varphi \)
l1
nfv
\( \vdash \Finv z \, \psi \)
dvelimnf.2
\( \vdash z = y \rightarrow (\varphi \leftrightarrow \psi) \)
dvelimf l0 l1 _