Description: Membership in a successor. Exercise 5 of TakeutiZaring p. 17. (Contributed by NM, 15-Sep-1995)
Ref | Expression | ||
---|---|---|---|
Assertion | elsucg | |- ( A 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 | 2 3 | bitri | |- ( A e. suc B <-> ( A e. B \/ A e. { B } ) ) |
5 | elsng | |- ( A e. V -> ( A e. { B } <-> A = B ) ) |
|
6 | 5 | orbi2d | |- ( A e. V -> ( ( A e. B \/ A e. { B } ) <-> ( A e. B \/ A = B ) ) ) |
7 | 4 6 | syl5bb | |- ( A e. V -> ( A e. suc B <-> ( A e. B \/ A = B ) ) ) |