Metamath Proof Explorer


Theorem wl-dfclab

Description: Rederive df-clab from wl-clabv . (Contributed by Wolf Lammen, 31-May-2023) (Proof modification is discouraged.)

Ref Expression
Assertion wl-dfclab xy|φxyφ

Proof

Step Hyp Ref Expression
1 dfclel xy|φzz=xzy|φ
2 wl-clabv zy|φzyφ
3 sbequ z=xzyφxyφ
4 2 3 bitrid z=xzy|φxyφ
5 4 pm5.32i z=xzy|φz=xxyφ
6 5 exbii zz=xzy|φzz=xxyφ
7 19.41v zz=xxyφzz=xxyφ
8 ax6ev zz=x
9 8 biantrur xyφzz=xxyφ
10 7 9 bitr4i zz=xxyφxyφ
11 1 6 10 3bitri xy|φxyφ