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

Theorem sucidg 5463
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 2428 . . 3  |-  A  =  A
21olci 392 . 2  |-  ( A  e.  A  \/  A  =  A )
3 elsucg 5452 . 2  |-  ( A  e.  V  ->  ( A  e.  suc  A  <->  ( A  e.  A  \/  A  =  A ) ) )
42, 3mpbiri 236 1  |-  ( A  e.  V  ->  A  e.  suc  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 369    = wceq 1437    e. wcel 1872   suc csuc 5387
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-v 3024  df-un 3384  df-sn 3942  df-suc 5391
This theorem is referenced by:  sucid  5464  nsuceq0  5465  trsuc  5469  sucssel  5477  ordsuc  6599  onpsssuc  6604  nlimsucg  6627  tfrlem11  7061  tfrlem13  7063  tz7.44-2  7080  omeulem1  7238  oeordi  7243  oeeulem  7257  php4  7712  wofib  8013  suc11reg  8077  cantnfle  8128  cantnflt2  8130  cantnfp1lem3  8137  cantnflem1  8146  dfac12lem1  8524  dfac12lem2  8525  ttukeylem3  8892  ttukeylem7  8896  r1wunlim  9113  ontgval  31040  sucneqond  31675  finxpreclem4  31693  finxpsuclem  31696
  Copyright terms: Public domain W3C validator