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 | |- ( B e. V -> ( A e. suc B <-> ( A e. B \/ A = B ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-suc | |- suc B = ( B u. { B } ) |
|
2 | 1 | eleq2i | |- ( A e. suc B <-> A e. ( B u. { B } ) ) |
3 | elun | |- ( A e. ( B u. { B } ) <-> ( A e. B \/ A e. { B } ) ) |
|
4 | elsn2g | |- ( B e. V -> ( A e. { B } <-> A = B ) ) |
|
5 | 4 | orbi2d | |- ( B e. V -> ( ( A e. B \/ A e. { B } ) <-> ( A e. B \/ A = B ) ) ) |
6 | 3 5 | bitrid | |- ( B e. V -> ( A e. ( B u. { B } ) <-> ( A e. B \/ A = B ) ) ) |
7 | 2 6 | bitrid | |- ( B e. V -> ( A e. suc B <-> ( A e. B \/ A = B ) ) ) |