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

Theorem elsuci 4649
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 4589 . . . 4  |-  suc  B  =  ( B  u.  { B } )
21eleq2i 2502 . . 3  |-  ( A  e.  suc  B  <->  A  e.  ( B  u.  { B } ) )
3 elun 3490 . . 3  |-  ( A  e.  ( B  u.  { B } )  <->  ( A  e.  B  \/  A  e.  { B } ) )
42, 3bitri 242 . 2  |-  ( A  e.  suc  B  <->  ( A  e.  B  \/  A  e.  { B } ) )
5 elsni 3840 . . 3  |-  ( A  e.  { B }  ->  A  =  B )
65orim2i 506 . 2  |-  ( ( A  e.  B  \/  A  e.  { B } )  ->  ( A  e.  B  \/  A  =  B )
)
74, 6sylbi 189 1  |-  ( A  e.  suc  B  -> 
( A  e.  B  \/  A  =  B
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 359    = wceq 1653    e. wcel 1726    u. cun 3320   {csn 3816   suc csuc 4585
This theorem is referenced by:  suctr  4667  trsucss  4669  ordnbtwn  4674  suc11  4687  tfrlem11  6651  omordi  6811  nnmordi  6876  phplem3  7290  pssnn  7329  r1sdom  7702  cfsuc  8139  axdc3lem2  8333  axdc3lem4  8335  indpi  8786  ontgval  26183  onsucconi  26189  suctrALT2VD  29010  suctrALT2  29011  suctrALTcf  29096  suctrALTcfVD  29097  suctrALT3  29098  bnj563  29173  bnj964  29376
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-un 3327  df-sn 3822  df-suc 4589
  Copyright terms: Public domain W3C validator