Theorem sbequ2

Description: An equality theorem for substitution. (Contributed by NM, 16-May-1993) Revise df-sb . (Revised by BJ, 22-Dec-2020) (Proof shortened by Wolf Lammen, 3-Feb-2024)

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

Proof

Step	Hyp	Ref	Expression
1		dfsbimp	|- ( [ t / x ] ph -> A. y ( y = t -> A. x ( x = y -> ph ) ) )
2		equvinva	|- ( x = t -> E. y ( x = y /\ t = y ) )
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	aleximi	|- ( A. y ( y = t -> A. x ( x = y -> ph ) ) -> ( E. y ( x = y /\ t = y ) -> E. y ph ) )
8	1 2 7	syl2im	|- ( [ t / x ] ph -> ( x = t -> E. y ph ) )
9		ax5e	|- ( E. y ph -> ph )
10	8 9	syl6com	|- ( x = t -> ( [ t / x ] ph -> ph ) )