Theorem spsbeOLD

Description: Obsolete version of spsbe as of 11-Jul-2023. (Contributed by NM, 29-Jun-1993) (Proof shortened by Wolf Lammen, 3-May-2018) Revise df-sb . (Revised by BJ, 22-Dec-2020) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	spsbeOLD	|- ( [ 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		ax6ev	|- E. y y = t
3		exim	|- ( A. y ( y = t -> A. x ( x = y -> ph ) ) -> ( E. y y = t -> E. y A. x ( x = y -> ph ) ) )
4	2 3	mpi	|- ( A. y ( y = t -> A. x ( x = y -> ph ) ) -> E. y A. x ( x = y -> ph ) )
5	1 4	sylbi	|- ( [ t / x ] ph -> E. y A. x ( x = y -> ph ) )
6		exim	|- ( A. x ( x = y -> ph ) -> ( E. x x = y -> E. x ph ) )
7	6	eximi	|- ( E. y A. x ( x = y -> ph ) -> E. y ( E. x x = y -> E. x ph ) )
8		ax6ev	|- E. x x = y
9		pm2.27	|- ( E. x x = y -> ( ( E. x x = y -> E. x ph ) -> E. x ph ) )
10	8 9	ax-mp	|- ( ( E. x x = y -> E. x ph ) -> E. x ph )
11	10	exlimiv	|- ( E. y ( E. x x = y -> E. x ph ) -> E. x ph )
12	5 7 11	3syl	|- ( [ t / x ] ph -> E. x ph )