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

Theorem sucidg 4469
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 2284 . . 3  |-  A  =  A
21olci 382 . 2  |-  ( A  e.  A  \/  A  =  A )
3 elsucg 4458 . 2  |-  ( A  e.  V  ->  ( A  e.  suc  A  <->  ( A  e.  A  \/  A  =  A ) ) )
42, 3mpbiri 226 1  |-  ( A  e.  V  ->  A  e.  suc  A )
Colors of variables: wff set class
Syntax hints:    -> wi 6    \/ wo 359    = wceq 1624    e. wcel 1685   suc csuc 4393
This theorem is referenced by:  sucid  4470  nsuceq0  4471  trsuc  4475  sucssel  4484  ordsuc  4604  onpsssuc  4609  nlimsucg  4632  tfrlem11  6399  tfrlem13  6401  tz7.44-2  6415  omeulem1  6575  oeordi  6580  oeeulem  6594  php4  7043  wofib  7255  suc11reg  7315  cantnfle  7367  cantnflt2  7369  cantnfp1lem3  7377  cantnflem1  7386  dfac12lem1  7764  dfac12lem2  7765  ttukeylem3  8133  ttukeylem7  8137  r1wunlim  8354  ontgval  24277
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-un 3158  df-sn 3647  df-suc 4397
  Copyright terms: Public domain W3C validator