Metamath Proof Explorer


Theorem sbequ2OLD

Description: Obsolete version of sbequ2 as of 3-Feb-2024. (Contributed by NM, 16-May-1993) (Proof shortened by Wolf Lammen, 25-Feb-2018) Revise df-sb . (Revised by BJ, 22-Dec-2020) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion sbequ2OLD x = t t x φ φ

Proof

Step Hyp Ref Expression
1 equvinva x = t y x = y t = y
2 df-sb t x φ y y = t x x = y φ
3 equcomi t = y y = t
4 sp x x = y φ x = y φ
5 3 4 imim12i y = t x x = y φ t = y x = y φ
6 5 impcomd y = t x x = y φ x = y t = y φ
7 6 alimi y y = t x x = y φ y x = y t = y φ
8 2 7 sylbi t x φ y x = y t = y φ
9 19.23v y x = y t = y φ y x = y t = y φ
10 8 9 sylib t x φ y x = y t = y φ
11 1 10 syl5com x = t t x φ φ