# 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 ) )`