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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-sb | |
|
2 | 1 | biimpi | |
3 | equvinva | |
|
4 | equcomi | |
|
5 | sp | |
|
6 | 4 5 | imim12i | |
7 | 6 | impcomd | |
8 | 7 | aleximi | |
9 | 2 3 8 | syl2im | |
10 | ax5e | |
|
11 | 9 10 | syl6com | |