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

Theorem elsuci 5492
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 5432 . . . 4  |-  suc  B  =  ( B  u.  { B } )
21eleq2i 2523 . . 3  |-  ( A  e.  suc  B  <->  A  e.  ( B  u.  { B } ) )
3 elun 3576 . . 3  |-  ( A  e.  ( B  u.  { B } )  <->  ( A  e.  B  \/  A  e.  { B } ) )
42, 3bitri 253 . 2  |-  ( A  e.  suc  B  <->  ( A  e.  B  \/  A  e.  { B } ) )
5 elsni 3995 . . 3  |-  ( A  e.  { B }  ->  A  =  B )
65orim2i 521 . 2  |-  ( ( A  e.  B  \/  A  e.  { B } )  ->  ( A  e.  B  \/  A  =  B )
)
74, 6sylbi 199 1  |-  ( A  e.  suc  B  -> 
( A  e.  B  \/  A  =  B
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 370    = wceq 1446    e. wcel 1889    u. cun 3404   {csn 3970   suc csuc 5428
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-v 3049  df-un 3411  df-sn 3971  df-suc 5432
This theorem is referenced by:  trsucss  5511  ordnbtwn  5516  suc11  5529  tfrlem11  7111  omordi  7272  nnmordi  7337  phplem3  7758  pssnn  7795  r1sdom  8250  cfsuc  8692  axdc3lem2  8886  axdc3lem4  8888  indpi  9337  bnj563  29565  bnj964  29766  ontgval  31103  onsucconi  31109  suctrALT  37232  suctrALT2VD  37242  suctrALT2  37243  suctrALTcf  37329  suctrALTcfVD  37330  suctrALT3  37331
  Copyright terms: Public domain W3C validator