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

Theorem elsuci 4933
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 4873 . . . 4  |-  suc  B  =  ( B  u.  { B } )
21eleq2i 2532 . . 3  |-  ( A  e.  suc  B  <->  A  e.  ( B  u.  { B } ) )
3 elun 3631 . . 3  |-  ( A  e.  ( B  u.  { B } )  <->  ( A  e.  B  \/  A  e.  { B } ) )
42, 3bitri 249 . 2  |-  ( A  e.  suc  B  <->  ( A  e.  B  \/  A  e.  { B } ) )
5 elsni 4041 . . 3  |-  ( A  e.  { B }  ->  A  =  B )
65orim2i 516 . 2  |-  ( ( A  e.  B  \/  A  e.  { B } )  ->  ( A  e.  B  \/  A  =  B )
)
74, 6sylbi 195 1  |-  ( A  e.  suc  B  -> 
( A  e.  B  \/  A  =  B
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 366    = wceq 1398    e. wcel 1823    u. cun 3459   {csn 4016   suc csuc 4869
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-un 3466  df-sn 4017  df-suc 4873
This theorem is referenced by:  trsucss  4952  ordnbtwn  4957  suc11  4970  tfrlem11  7049  omordi  7207  nnmordi  7272  phplem3  7691  pssnn  7731  r1sdom  8183  cfsuc  8628  axdc3lem2  8822  axdc3lem4  8824  indpi  9274  ontgval  30124  onsucconi  30130  suctrALT  34026  suctrALT2VD  34036  suctrALT2  34037  suctrALTcf  34123  suctrALTcfVD  34124  suctrALT3  34125  bnj563  34201  bnj964  34402
  Copyright terms: Public domain W3C validator