Theorem elsuci 4933

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 4873	. . . 4 |- suc B = ( B u. { B } )
2	1	eleq2i 2532	. . 3 |- ( A e. suc B <-> A e. ( B u. { B } ) )
3		elun 3631	. . 3 |- ( A e. ( B u. { B } ) <-> ( A e. B \/ A e. { B } ) )
4	2, 3	bitri 249	. 2 |- ( A e. suc B <-> ( A e. B \/ A e. { B } ) )
5		elsni 4041	. . 3 |- ( A e. { B } -> A = B )
6	5	orim2i 516	. 2 |- ( ( A e. B \/ A e. { B } ) -> ( A e. B \/ A = B ) )
7	4, 6	sylbi 195	1 |- ( A e. suc B -> ( A e. B \/ A = B ) )

Syntax hints:   -> wi 4   \/ wo 366   = wceq 1398   e. wcel 1823   u. cun 3459   {csn 4016   suc csuc 4869

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-un 3466  df-sn 4017  df-suc 4873

This theorem is referenced by:  trsucss  4952  ordnbtwn  4957  suc11  4970  tfrlem11  7049  omordi  7207  nnmordi  7272  phplem3  7691  pssnn  7731  r1sdom  8183  cfsuc  8628  axdc3lem2  8822  axdc3lem4  8824  indpi  9274  ontgval  30124  onsucconi  30130  suctrALT  34026  suctrALT2VD  34036  suctrALT2  34037  suctrALTcf  34123  suctrALTcfVD  34124  suctrALT3  34125  bnj563  34201  bnj964  34402