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φtxφ

Proof

Step Hyp Ref Expression
1 equeucl x=ty=tx=y
2 ax12v x=yφxx=yφ
3 1 2 syl6 x=ty=tφxx=yφ
4 3 com23 x=tφy=txx=yφ
5 4 alrimdv x=tφyy=txx=yφ
6 df-sb txφyy=txx=yφ
7 5 6 imbitrrdi x=tφtxφ