This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 dfsb 
 |-  ( [ 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 )