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=ttxφφ

Proof

Step Hyp Ref Expression
1 df-sb txφyy=txx=yφ
2 1 biimpi txφyy=txx=yφ
3 equvinva x=tyx=yt=y
4 equcomi t=yy=t
5 sp xx=yφx=yφ
6 4 5 imim12i y=txx=yφt=yx=yφ
7 6 impcomd y=txx=yφx=yt=yφ
8 7 aleximi yy=txx=yφyx=yt=yyφ
9 2 3 8 syl2im txφx=tyφ
10 ax5e yφφ
11 9 10 syl6com x=ttxφφ