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

Theorem sucidg 6241
 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 2801 . . 3 𝐴 = 𝐴
21olci 863 . 2 (𝐴𝐴𝐴 = 𝐴)
3 elsucg 6230 . 2 (𝐴𝑉 → (𝐴 ∈ suc 𝐴 ↔ (𝐴𝐴𝐴 = 𝐴)))
42, 3mpbiri 261 1 (𝐴𝑉𝐴 ∈ suc 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ wo 844   = wceq 1538   ∈ wcel 2112  suc csuc 6165 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-un 3889  df-sn 4529  df-suc 6169 This theorem is referenced by:  sucid  6242  nsuceq0  6243  trsuc  6247  sucssel  6255  ordsuc  7513  onpsssuc  7518  nlimsucg  7541  tfrlem11  8011  tfrlem13  8013  tz7.44-2  8030  omeulem1  8195  oeordi  8200  oeeulem  8214  php4  8692  wofib  8997  suc11reg  9070  cantnfle  9122  cantnflt2  9124  cantnfp1lem3  9131  cantnflem1  9140  dfac12lem1  9558  dfac12lem2  9559  ttukeylem3  9926  ttukeylem7  9930  r1wunlim  10152  fmla  32742  ex-sategoelelomsuc  32787  noresle  33314  noprefixmo  33316  ontgval  33893  sucneqond  34783  finxpreclem4  34812  finxpsuclem  34815
 Copyright terms: Public domain W3C validator