Theorem spimt
Closed theorem form of spim. (Contributed by NM, 15-Jan-2008.)
(Revised by Mario Carneiro, 17-Oct-2016.) (Proof shortened by Wolf
Lammen, 21-Mar-2023.) Usage of this theorem is discouraged because it
depends on [ax-13]. (New usage is discouraged.)
Conclusion
\( \vdash \Finv x \, \psi \wedge \forall x \, (x = y' \rightarrow \varphi \rightarrow \psi) \rightarrow \forall x \, \varphi \rightarrow \psi \)
Proof
l0
ax6e
\( \vdash \exists x \, x = y' \)
exim
\( \vdash \forall x \, (x = y' \rightarrow \varphi \rightarrow \psi) \rightarrow \exists x \, x = y' \rightarrow \exists x \, (\varphi \rightarrow \psi) \)
l2
mpi l0 _
\( \vdash \forall x \, (x = y' \rightarrow \varphi \rightarrow \psi) \rightarrow \exists x \, (\varphi \rightarrow \psi) \)
19.35
\( \vdash \exists x \, (\varphi \rightarrow \psi) \leftrightarrow \forall x \, \varphi \rightarrow \exists x \, \psi \)
l4
sylib l2 _
\( \vdash \forall x \, (x = y' \rightarrow \varphi \rightarrow \psi) \rightarrow \forall x \, \varphi \rightarrow \exists x \, \psi \)
id
19.9d _
\( \vdash \Finv x \, \psi \rightarrow \exists x \, \psi \rightarrow \psi \)
sylan9r l4 _