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 or be sets. (Contributed by NM, 6-Jun-1994.)
Assertion
Ref Expression
elsuci

Proof of Theorem elsuci
StepHypRef Expression
1 df-suc 4579 . . . 4
21eleq2i 2499 . . 3
3 elun 3480 . . 3
42, 3bitri 241 . 2
5 elsni 3830 . . 3
65orim2i 505 . 2
74, 6sylbi 188 1
 Colors of variables: wff set class Syntax hints:   wi 4   wo 358   wceq 1652   wcel 1725   cun 3310  csn 3806   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