Theorem dvelimhw
Proof of dvelimh without using [ax-13] but with additional distinct
variable conditions. (Contributed by NM, 1-Oct-2002.) (Revised by
Andrew Salmon, 21-Jul-2011.) (Revised by NM, 1-Aug-2017.) (Proof
shortened by Wolf Lammen, 23-Dec-2018.)
Hypotheses
dvelimhw.1
\( \vdash \varphi \rightarrow \forall x \, \varphi \)
dvelimhw.2
\( \vdash \psi \rightarrow \forall z \, \psi \)
dvelimhw.3
\( \vdash z = y' \rightarrow (\varphi \leftrightarrow \psi) \)
dvelimhw.4
\( \vdash \neg \forall x \, x = y' \rightarrow y' = z \rightarrow \forall x \, y' = z \)
Conclusion
\( \vdash \neg \forall x \, x = y' \rightarrow \psi \rightarrow \forall x \, \psi \)
Proof
l0
nfv
l1
equcom
\( \vdash z = y' \leftrightarrow y' = z \)
l2
nfna1
dvelimhw.4
nf5d l2 _
\( \vdash \neg \forall x \, x = y' \rightarrow \Finv x \, y' = z \)
l5
nfxfrd l1 _
dvelimhw.1
nf5i _
a1i _
nfimd l5 _
l10
nfald l0 _
\( \vdash \neg \forall x \, x = y' \rightarrow \Finv x \, \forall z \, (z = y' \rightarrow \varphi) \)
l11
dvelimhw.2
dvelimhw.3
equsalhw l11 _
nfbii _
\( \vdash \Finv x \, \forall z \, (z = y' \rightarrow \varphi) \leftrightarrow \Finv x \, \psi \)
sylib l10 _
nf5rd _