Theorem dvelimdf
Deduction form of dvelimf. Usage of this theorem is discouraged
because it depends on [ax-13]. (Contributed by NM, 7-Apr-2004.)
(Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf
Lammen, 11-May-2018.) (New usage is discouraged.)
Hypotheses
dvelimdf.1
\( \vdash \Finv x \, \varphi \)
dvelimdf.2
\( \vdash \Finv z \, \varphi \)
dvelimdf.3
\( \vdash \varphi \rightarrow \Finv x \, \psi \)
dvelimdf.4
\( \vdash \varphi \rightarrow \Finv z \, \chi \)
dvelimdf.5
\( \vdash \varphi \rightarrow z = y \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow \neg \forall x \, x = y \rightarrow \Finv x \, \chi \)
Proof
l0
dvelimdf.1
dvelimdf.3
l2
nfim1 l0 _
\( \vdash \Finv x \, (\varphi \rightarrow \psi) \)
l3
dvelimdf.2
dvelimdf.4
l5
nfim1 l3 _
\( \vdash \Finv z \, (\varphi \rightarrow \chi) \)
dvelimdf.5
com12 _
pm5.74d _
\( \vdash z = y \rightarrow (\varphi \rightarrow \psi \leftrightarrow \varphi \rightarrow \chi) \)
l9
dvelimf l2 l5 _
\( \vdash \neg \forall x \, x = y \rightarrow \Finv x \, (\varphi \rightarrow \chi) \)
l10
dvelimdf.1
pm5.5
nfbidf l10 _
\( \vdash \varphi \rightarrow (\Finv x \, (\varphi \rightarrow \chi) \leftrightarrow \Finv x \, \chi) \)
imbitrid l9 _