Theorem elsuci 5505

Description: Membership in a successor. This one-way implication does not require that either A or B be sets. (Contributed by NM, 6-Jun-1994.)

Assertion

Ref	Expression
elsuci	|- ( A e. suc B -> ( A e. B \/ A = B ) )

Proof of Theorem elsuci

Step	Hyp	Ref	Expression
1		df-suc 5445	. . . 4 |- suc B = ( B u. { B } )
2	1	eleq2i 2500	. . 3 |- ( A e. suc B <-> A e. ( B u. { B } ) )
3		elun 3606	. . 3 |- ( A e. ( B u. { B } ) <-> ( A e. B \/ A e. { B } ) )
4	2, 3	bitri 252	. 2 |- ( A e. suc B <-> ( A e. B \/ A e. { B } ) )
5		elsni 4021	. . 3 |- ( A e. { B } -> A = B )
6	5	orim2i 520	. 2 |- ( ( A e. B \/ A e. { B } ) -> ( A e. B \/ A = B ) )
7	4, 6	sylbi 198	1 |- ( A e. suc B -> ( A e. B \/ A = B ) )

Syntax hints:   -> wi 4   \/ wo 369   = wceq 1437   e. wcel 1868   u. cun 3434   {csn 3996   suc csuc 5441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-v 3083  df-un 3441  df-sn 3997  df-suc 5445

This theorem is referenced by:  trsucss  5524  ordnbtwn  5529  suc11  5542  tfrlem11  7111  omordi  7272  nnmordi  7337  phplem3  7756  pssnn  7793  r1sdom  8247  cfsuc  8688  axdc3lem2  8882  axdc3lem4  8884  indpi  9333  bnj563  29549  bnj964  29750  ontgval  31084  onsucconi  31090  suctrALT  37083  suctrALT2VD  37093  suctrALT2  37094  suctrALTcf  37180  suctrALTcfVD  37181  suctrALT3  37182