Description: Membership of a class abstraction in another class. (Contributed by NM, 17-Jan-2006)
Ref | Expression | ||
---|---|---|---|
Assertion | clabel | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfclel | |
|
2 | abeq2 | |
|
3 | 2 | anbi2ci | |
4 | 3 | exbii | |
5 | 1 4 | bitri | |