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

Metamath Proof Explorer

Theorem sb4a

Description: A version of one implication of sb4b that does not require a distinctor antecedent. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker sb4av when possible. (Contributed by NM, 2-Feb-2007) Revise df-sb . (Revised by Wolf Lammen, 28-Jul-2023) (New usage is discouraged.)

Ref Expression
Assertion sb4a 
|- ( [ t / x ] A. t ph -> A. x ( x = t -> ph ) )

Proof

Step Hyp Ref Expression
1 sbequ2 
 |-  ( x = t -> ( [ t / x ] A. t ph -> A. t ph ) )
2 1 sps 
 |-  ( A. x x = t -> ( [ t / x ] A. t ph -> A. t ph ) )
3 axc11r 
 |-  ( A. x x = t -> ( A. t ph -> A. x ph ) )
4 ala1 
 |-  ( A. x ph -> A. x ( x = t -> ph ) )
5 3 4 syl6 
 |-  ( A. x x = t -> ( A. t ph -> A. x ( x = t -> ph ) ) )
6 2 5 syld 
 |-  ( A. x x = t -> ( [ t / x ] A. t ph -> A. x ( x = t -> ph ) ) )
7 sb4b 
 |-  ( -. A. x x = t -> ( [ t / x ] A. t ph <-> A. x ( x = t -> A. t ph ) ) )
8 sp 
 |-  ( A. t ph -> ph )
9 8 imim2i 
 |-  ( ( x = t -> A. t ph ) -> ( x = t -> ph ) )
10 9 alimi 
 |-  ( A. x ( x = t -> A. t ph ) -> A. x ( x = t -> ph ) )
11 7 10 biimtrdi 
 |-  ( -. A. x x = t -> ( [ t / x ] A. t ph -> A. x ( x = t -> ph ) ) )
12 6 11 pm2.61i 
 |-  ( [ t / x ] A. t ph -> A. x ( x = t -> ph ) )