Theorem spsbe

Description: 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)

	Ref	Expression
Assertion	spsbe	|- ( [ t / x ] ph -> E. x ph )

Proof

Step	Hyp	Ref	Expression
1		df-sb	|- ( [ t / x ] ph <-> A. y ( y = t -> A. x ( x = y -> ph ) ) )
2		alequexv	|- ( A. y ( y = t -> A. x ( x = y -> ph ) ) -> E. y A. x ( x = y -> ph ) )
3		exsbim	|- ( E. y A. x ( x = y -> ph ) -> E. x ph )
4	2 3	syl	|- ( A. y ( y = t -> A. x ( x = y -> ph ) ) -> E. x ph )
5	1 4	sylbi	|- ( [ t / x ] ph -> E. x ph )