Metamath Proof Explorer


Theorem elsucg

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 ) ) )

Proof

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 ) ) )