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

Theorem sucidg 4470
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 2283 . . 3  |-  A  =  A
21olci 380 . 2  |-  ( A  e.  A  \/  A  =  A )
3 elsucg 4459 . 2  |-  ( A  e.  V  ->  ( A  e.  suc  A  <->  ( A  e.  A  \/  A  =  A ) ) )
42, 3mpbiri 224 1  |-  ( A  e.  V  ->  A  e.  suc  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 357    = wceq 1623    e. wcel 1684   suc csuc 4394
This theorem is referenced by:  sucid  4471  nsuceq0  4472  trsuc  4476  sucssel  4485  ordsuc  4605  onpsssuc  4610  nlimsucg  4633  tfrlem11  6404  tfrlem13  6406  tz7.44-2  6420  omeulem1  6580  oeordi  6585  oeeulem  6599  php4  7048  wofib  7260  suc11reg  7320  cantnfle  7372  cantnflt2  7374  cantnfp1lem3  7382  cantnflem1  7391  dfac12lem1  7769  dfac12lem2  7770  ttukeylem3  8138  ttukeylem7  8142  r1wunlim  8359  ontgval  24870
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157  df-sn 3646  df-suc 4398
  Copyright terms: Public domain W3C validator