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

Theorem elsuci 4460
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 4400 . . . 4  |-  suc  B  =  ( B  u.  { B } )
21eleq2i 2349 . . 3  |-  ( A  e.  suc  B  <->  A  e.  ( B  u.  { B } ) )
3 elun 3318 . . 3  |-  ( A  e.  ( B  u.  { B } )  <->  ( A  e.  B  \/  A  e.  { B } ) )
42, 3bitri 240 . 2  |-  ( A  e.  suc  B  <->  ( A  e.  B  \/  A  e.  { B } ) )
5 elsni 3666 . . 3  |-  ( A  e.  { B }  ->  A  =  B )
65orim2i 504 . 2  |-  ( ( A  e.  B  \/  A  e.  { B } )  ->  ( A  e.  B  \/  A  =  B )
)
74, 6sylbi 187 1  |-  ( A  e.  suc  B  -> 
( A  e.  B  \/  A  =  B
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 357    = wceq 1625    e. wcel 1686    u. cun 3152   {csn 3642   suc csuc 4396
This theorem is referenced by:  trsucss  4480  ordnbtwn  4485  suc11  4498  tfrlem11  6406  omordi  6566  nnmordi  6631  phplem3  7044  pssnn  7083  r1sdom  7448  cfsuc  7885  axdc3lem2  8079  axdc3lem4  8081  indpi  8533  ontgval  24872  onsucconi  24878  suctrALT2VD  28685  suctrALT2  28686  suctrALTcf  28771  suctrALTcfVD  28772  suctrALT3  28773  suctrALT4  28777  bnj563  28845  bnj964  29048
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792  df-un 3159  df-sn 3648  df-suc 4400
  Copyright terms: Public domain W3C validator