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

Theorem sucidg 5944
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 2771 . . 3 𝐴 = 𝐴
21olci 855 . 2 (𝐴𝐴𝐴 = 𝐴)
3 elsucg 5933 . 2 (𝐴𝑉 → (𝐴 ∈ suc 𝐴 ↔ (𝐴𝐴𝐴 = 𝐴)))
42, 3mpbiri 248 1 (𝐴𝑉𝐴 ∈ suc 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 836   = wceq 1631  wcel 2145  suc csuc 5866
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-un 3728  df-sn 4317  df-suc 5870
This theorem is referenced by:  sucid  5945  nsuceq0  5946  trsuc  5951  sucssel  5960  ordsuc  7159  onpsssuc  7164  nlimsucg  7187  tfrlem11  7635  tfrlem13  7637  tz7.44-2  7654  omeulem1  7814  oeordi  7819  oeeulem  7833  php4  8301  wofib  8604  suc11reg  8678  cantnfle  8730  cantnflt2  8732  cantnfp1lem3  8739  cantnflem1  8748  dfac12lem1  9165  dfac12lem2  9166  ttukeylem3  9533  ttukeylem7  9537  r1wunlim  9759  noresle  32176  noprefixmo  32178  ontgval  32760  sucneqond  33543  finxpreclem4  33561  finxpsuclem  33564
  Copyright terms: Public domain W3C validator