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

Theorem sucidg 5965
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 (𝐴𝑉𝐴 ∈ suc 𝐴)

Proof of Theorem sucidg
StepHypRef Expression
1 eqid 2761 . . 3 𝐴 = 𝐴
21olci 405 . 2 (𝐴𝐴𝐴 = 𝐴)
3 elsucg 5954 . 2 (𝐴𝑉 → (𝐴 ∈ suc 𝐴 ↔ (𝐴𝐴𝐴 = 𝐴)))
42, 3mpbiri 248 1 (𝐴𝑉𝐴 ∈ suc 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 382   = wceq 1632  wcel 2140  suc csuc 5887
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-v 3343  df-un 3721  df-sn 4323  df-suc 5891
This theorem is referenced by:  sucid  5966  nsuceq0  5967  trsuc  5972  sucssel  5981  ordsuc  7181  onpsssuc  7186  nlimsucg  7209  tfrlem11  7655  tfrlem13  7657  tz7.44-2  7674  omeulem1  7834  oeordi  7839  oeeulem  7853  php4  8315  wofib  8618  suc11reg  8692  cantnfle  8744  cantnflt2  8746  cantnfp1lem3  8753  cantnflem1  8762  dfac12lem1  9178  dfac12lem2  9179  ttukeylem3  9546  ttukeylem7  9550  r1wunlim  9772  noresle  32174  noprefixmo  32176  ontgval  32758  sucneqond  33543  finxpreclem4  33561  finxpsuclem  33564
  Copyright terms: Public domain W3C validator