Metamath Proof Explorer

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 df-sb 
 |-  ( [ t / x ] ph <-> A. y ( y = t -> A. x ( x = y -> ph ) ) )
2 1 biimpi 
 |-  ( [ t / x ] ph -> A. y ( y = t -> A. x ( x = y -> ph ) ) )
3 equvinva 
 |-  ( x = t -> E. y ( x = y /\ t = y ) )
4 equcomi 
 |-  ( t = y -> y = t )
5 sp 
 |-  ( A. x ( x = y -> ph ) -> ( x = y -> ph ) )
6 4 5 imim12i 
 |-  ( ( y = t -> A. x ( x = y -> ph ) ) -> ( t = y -> ( x = y -> ph ) ) )
7 6 impcomd 
 |-  ( ( y = t -> A. x ( x = y -> ph ) ) -> ( ( x = y /\ t = y ) -> ph ) )
8 7 aleximi 
 |-  ( A. y ( y = t -> A. x ( x = y -> ph ) ) -> ( E. y ( x = y /\ t = y ) -> E. y ph ) )
9 2 3 8 syl2im 
 |-  ( [ t / x ] ph -> ( x = t -> E. y ph ) )
10 ax5e 
 |-  ( E. y ph -> ph )
11 9 10 syl6com 
 |-  ( x = t -> ( [ t / x ] ph -> ph ) )