Theorem spsbe
Existential generalization: if a proposition is true for a specific
instance, then there exists an instance where it is true. (Contributed
by NM, 29-Jun-1993.) (Proof shortened by Wolf Lammen, 3-May-2018.)
Revise [df-sb]. (Revised by BJ, 22-Dec-2020.) (Proof shortened by
Steven Nguyen, 11-Jul-2023.)
Conclusion
\( \vdash [ t' / x ] \, \varphi \rightarrow \exists x \, \varphi \)
Proof
l0
dfsb
\( \vdash [ t' / x ] \, \varphi \leftrightarrow \forall y \, (y = t' \rightarrow \forall x \, (x = y \rightarrow \varphi)) \)
alequexv
\( \vdash \forall y \, (y = t' \rightarrow \forall x \, (x = y \rightarrow \varphi)) \rightarrow \exists y \, \forall x \, (x = y \rightarrow \varphi) \)
l2
sylbi l0 _
\( \vdash [ t' / x ] \, \varphi \rightarrow \exists y \, \forall x \, (x = y \rightarrow \varphi) \)
exsbim
\( \vdash \exists y \, \forall x \, (x = y \rightarrow \varphi) \rightarrow \exists x \, \varphi \)
syl l2 _