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

Theorem elsuci 4458
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 4398 . . . 4  |-  suc  B  =  ( B  u.  { B } )
21eleq2i 2347 . . 3  |-  ( A  e.  suc  B  <->  A  e.  ( B  u.  { B } ) )
3 elun 3316 . . 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 3664 . . 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 1623    e. wcel 1684    u. cun 3150   {csn 3640   suc csuc 4394
This theorem is referenced by:  trsucss  4478  ordnbtwn  4483  suc11  4496  tfrlem11  6404  omordi  6564  nnmordi  6629  phplem3  7042  pssnn  7081  r1sdom  7446  cfsuc  7883  axdc3lem2  8077  axdc3lem4  8079  indpi  8531  ontgval  24870  onsucconi  24876  suctrALT2VD  28612  suctrALT2  28613  suctrALTcf  28698  suctrALTcfVD  28699  suctrALT3  28700  suctrALT4  28704  bnj563  28772  bnj964  28975
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157  df-sn 3646  df-suc 4398
  Copyright terms: Public domain W3C validator