Metamath Proof Explorer

Theorem sbequ1

Description: An equality theorem for substitution. (Contributed by NM, 16-May-1993) Revise df-sb . (Revised by BJ, 22-Dec-2020)

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

Proof

Step Hyp Ref Expression
1 equeucl 
 |-  ( x = t -> ( y = t -> x = y ) )
2 ax12v 
 |-  ( x = y -> ( ph -> A. x ( x = y -> ph ) ) )
3 1 2 syl6 
 |-  ( x = t -> ( y = t -> ( ph -> A. x ( x = y -> ph ) ) ) )
4 3 com23 
 |-  ( x = t -> ( ph -> ( y = t -> A. x ( x = y -> ph ) ) ) )
5 4 alrimdv 
 |-  ( x = t -> ( ph -> A. y ( y = t -> A. x ( x = y -> ph ) ) ) )
6 df-sb 
 |-  ( [ t / x ] ph <-> A. y ( y = t -> A. x ( x = y -> ph ) ) )
7 5 6 imbitrrdi 
 |-  ( x = t -> ( ph -> [ t / x ] ph ) )