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

Theorem sucidg 4956
Description: Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized). (Contributed by NM, 25-Mar-1995.) (Proof shortened by Scott Fenton, 20-Feb-2012.)
Assertion
Ref Expression
sucidg  |-  ( A  e.  V  ->  A  e.  suc  A )

Proof of Theorem sucidg
StepHypRef Expression
1 eqid 2467 . . 3  |-  A  =  A
21olci 391 . 2  |-  ( A  e.  A  \/  A  =  A )
3 elsucg 4945 . 2  |-  ( A  e.  V  ->  ( A  e.  suc  A  <->  ( A  e.  A  \/  A  =  A ) ) )
42, 3mpbiri 233 1  |-  ( A  e.  V  ->  A  e.  suc  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 368    = wceq 1379    e. wcel 1767   suc csuc 4880
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-un 3481  df-sn 4028  df-suc 4884
This theorem is referenced by:  sucid  4957  nsuceq0  4958  trsuc  4962  sucssel  4970  ordsuc  6627  onpsssuc  6632  nlimsucg  6655  tfrlem11  7054  tfrlem13  7056  tz7.44-2  7070  omeulem1  7228  oeordi  7233  oeeulem  7247  php4  7701  wofib  7966  suc11reg  8032  cantnfle  8086  cantnflt2  8088  cantnfp1lem3  8095  cantnflem1  8104  cantnfleOLD  8116  cantnflt2OLD  8118  cantnfp1lem3OLD  8121  cantnflem1OLD  8127  dfac12lem1  8519  dfac12lem2  8520  ttukeylem3  8887  ttukeylem7  8891  r1wunlim  9111  ontgval  29473
  Copyright terms: Public domain W3C validator