Description: Variant of membership in a successor, requiring that B rather than A be a set. (Contributed by NM, 28-Oct-2003)
Ref | Expression | ||
---|---|---|---|
Assertion | elsuc2g |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-suc | ||
2 | 1 | eleq2i | |
3 | elun | ||
4 | elsn2g | ||
5 | 4 | orbi2d | |
6 | 3 5 | syl5bb | |
7 | 2 6 | syl5bb |