Theorem 19.8aw

If a formula is true, then it is true for at least one instance. This is to 19.8a what spw is to sp. (Contributed by SN, 26-Sep-2024.)

Hypothesis
19.8aw.1
\( \vdash x = y \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \varphi \rightarrow \exists x \, \varphi \)
Proof
l0
alnex
\( \vdash \forall x \, \neg \varphi \leftrightarrow \neg \exists x \, \varphi \)
19.8aw.1
notbid _
\( \vdash x = y \rightarrow (\neg \varphi \leftrightarrow \neg \psi) \)
spw _
\( \vdash \forall x \, \neg \varphi \rightarrow \neg \varphi \)
sylbir l0 _
con4i _