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

Theorem elsuci 4639
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 4579 . . . 4  |-  suc  B  =  ( B  u.  { B } )
21eleq2i 2499 . . 3  |-  ( A  e.  suc  B  <->  A  e.  ( B  u.  { B } ) )
3 elun 3480 . . 3  |-  ( A  e.  ( B  u.  { B } )  <->  ( A  e.  B  \/  A  e.  { B } ) )
42, 3bitri 241 . 2  |-  ( A  e.  suc  B  <->  ( A  e.  B  \/  A  e.  { B } ) )
5 elsni 3830 . . 3  |-  ( A  e.  { B }  ->  A  =  B )
65orim2i 505 . 2  |-  ( ( A  e.  B  \/  A  e.  { B } )  ->  ( A  e.  B  \/  A  =  B )
)
74, 6sylbi 188 1  |-  ( A  e.  suc  B  -> 
( A  e.  B  \/  A  =  B
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 358    = wceq 1652    e. wcel 1725    u. cun 3310   {csn 3806   suc csuc 4575
This theorem is referenced by:  suctr  4657  trsucss  4659  ordnbtwn  4664  suc11  4677  tfrlem11  6641  omordi  6801  nnmordi  6866  phplem3  7280  pssnn  7319  r1sdom  7692  cfsuc  8129  axdc3lem2  8323  axdc3lem4  8325  indpi  8776  ontgval  26173  onsucconi  26179  suctrALT2VD  28885  suctrALT2  28886  suctrALTcf  28971  suctrALTcfVD  28972  suctrALT3  28973  bnj563  29048  bnj964  29251
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-un 3317  df-sn 3812  df-suc 4579
  Copyright terms: Public domain W3C validator