Theorem sbequ2OLD

Description: Obsolete version of sbequ2 as of 3-Feb-2024. (Contributed by NM, 16-May-1993) (Proof shortened by Wolf Lammen, 25-Feb-2018) Revise df-sb . (Revised by BJ, 22-Dec-2020) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	sbequ2OLD	|- ( x = t -> ( [ t / x ] ph -> ph ) )

Proof

Step	Hyp	Ref	Expression
1		equvinva	|- ( x = t -> E. y ( x = y /\ t = y ) )
2		df-sb	|- ( [ t / x ] ph <-> A. y ( y = t -> A. x ( x = y -> ph ) ) )
3		equcomi	|- ( t = y -> y = t )
4		sp	|- ( A. x ( x = y -> ph ) -> ( x = y -> ph ) )
5	3 4	imim12i	|- ( ( y = t -> A. x ( x = y -> ph ) ) -> ( t = y -> ( x = y -> ph ) ) )
6	5	impcomd	|- ( ( y = t -> A. x ( x = y -> ph ) ) -> ( ( x = y /\ t = y ) -> ph ) )
7	6	alimi	|- ( A. y ( y = t -> A. x ( x = y -> ph ) ) -> A. y ( ( x = y /\ t = y ) -> ph ) )
8	2 7	sylbi	|- ( [ t / x ] ph -> A. y ( ( x = y /\ t = y ) -> ph ) )
9		19.23v	|- ( A. y ( ( x = y /\ t = y ) -> ph ) <-> ( E. y ( x = y /\ t = y ) -> ph ) )
10	8 9	sylib	|- ( [ t / x ] ph -> ( E. y ( x = y /\ t = y ) -> ph ) )
11	1 10	syl5com	|- ( x = t -> ( [ t / x ] ph -> ph ) )