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

Theorem sucidg 4651
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 2435 . . 3  |-  A  =  A
21olci 381 . 2  |-  ( A  e.  A  \/  A  =  A )
3 elsucg 4640 . 2  |-  ( A  e.  V  ->  ( A  e.  suc  A  <->  ( A  e.  A  \/  A  =  A ) ) )
42, 3mpbiri 225 1  |-  ( A  e.  V  ->  A  e.  suc  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 358    = wceq 1652    e. wcel 1725   suc csuc 4575
This theorem is referenced by:  sucid  4652  nsuceq0  4653  trsuc  4657  sucssel  4665  ordsuc  4785  onpsssuc  4790  nlimsucg  4813  tfrlem11  6640  tfrlem13  6642  tz7.44-2  6656  omeulem1  6816  oeordi  6821  oeeulem  6835  php4  7285  wofib  7503  suc11reg  7563  cantnfle  7615  cantnflt2  7617  cantnfp1lem3  7625  cantnflem1  7634  dfac12lem1  8012  dfac12lem2  8013  ttukeylem3  8380  ttukeylem7  8384  r1wunlim  8601  ontgval  26129
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-un 3317  df-sn 3812  df-suc 4579
  Copyright terms: Public domain W3C validator