Theorem bj-ssbid2ALT

Description: Alternate proof of bj-ssbid2 , not using sbequ2 . (Contributed by BJ, 22-Dec-2020) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	bj-ssbid2ALT	|- ( [ x / x ] ph -> ph )

Proof

Step	Hyp	Ref	Expression
1		df-sb	|- ( [ x / x ] ph <-> A. y ( y = x -> A. x ( x = y -> ph ) ) )
2		sp	|- ( A. x ( x = y -> ph ) -> ( x = y -> ph ) )
3	2	imim2i	|- ( ( y = x -> A. x ( x = y -> ph ) ) -> ( y = x -> ( x = y -> ph ) ) )
4	3	alimi	|- ( A. y ( y = x -> A. x ( x = y -> ph ) ) -> A. y ( y = x -> ( x = y -> ph ) ) )
5		pm2.21	|- ( -. y = x -> ( y = x -> ph ) )
6		equcomi	|- ( y = x -> x = y )
7	6	imim1i	|- ( ( x = y -> ph ) -> ( y = x -> ph ) )
8	5 7	ja	|- ( ( y = x -> ( x = y -> ph ) ) -> ( y = x -> ph ) )
9	8	alimi	|- ( A. y ( y = x -> ( x = y -> ph ) ) -> A. y ( y = x -> ph ) )
10		ax6ev	|- E. y y = x
11		19.23v	|- ( A. y ( y = x -> ph ) <-> ( E. y y = x -> ph ) )
12	11	biimpi	|- ( A. y ( y = x -> ph ) -> ( E. y y = x -> ph ) )
13	9 10 12	mpisyl	|- ( A. y ( y = x -> ( x = y -> ph ) ) -> ph )
14	4 13	syl	|- ( A. y ( y = x -> A. x ( x = y -> ph ) ) -> ph )
15	1 14	sylbi	|- ( [ x / x ] ph -> ph )