MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elsuci Structured version   Unicode version

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
StepHypRef Expression
1 df-suc 5445 . . . 4  |-  suc  B  =  ( B  u.  { B } )
21eleq2i 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 } ) )
42, 3bitri 252 . 2  |-  ( A  e.  suc  B  <->  ( A  e.  B  \/  A  e.  { B } ) )
5 elsni 4021 . . 3  |-  ( A  e.  { B }  ->  A  =  B )
65orim2i 520 . 2  |-  ( ( A  e.  B  \/  A  e.  { B } )  ->  ( A  e.  B  \/  A  =  B )
)
74, 6sylbi 198 1  |-  ( A  e.  suc  B  -> 
( A  e.  B  \/  A  =  B
) )
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator