Description: Rederive df-clab from wl-clabv . (Contributed by Wolf Lammen, 31-May-2023) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | wl-dfclab | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfclel | |
|
2 | wl-clabv | |
|
3 | sbequ | |
|
4 | 2 3 | bitrid | |
5 | 4 | pm5.32i | |
6 | 5 | exbii | |
7 | 19.41v | |
|
8 | ax6ev | |
|
9 | 8 | biantrur | |
10 | 7 9 | bitr4i | |
11 | 1 6 10 | 3bitri | |