Metamath Proof Explorer


Theorem clabel

Description: Membership of a class abstraction in another class. (Contributed by NM, 17-Jan-2006)

Ref Expression
Assertion clabel x|φAyyAxxyφ

Proof

Step Hyp Ref Expression
1 dfclel x|φAyy=x|φyA
2 abeq2 y=x|φxxyφ
3 2 anbi2ci y=x|φyAyAxxyφ
4 3 exbii yy=x|φyAyyAxxyφ
5 1 4 bitri x|φAyyAxxyφ