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

Theorem sucidg 6112
 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 2780 . . 3 𝐴 = 𝐴
21olci 853 . 2 (𝐴𝐴𝐴 = 𝐴)
3 elsucg 6101 . 2 (𝐴𝑉 → (𝐴 ∈ suc 𝐴 ↔ (𝐴𝐴𝐴 = 𝐴)))
42, 3mpbiri 250 1 (𝐴𝑉𝐴 ∈ suc 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ wo 834   = wceq 1508   ∈ wcel 2051  suc csuc 6036 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2752 This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2761  df-cleq 2773  df-clel 2848  df-nfc 2920  df-v 3419  df-un 3836  df-sn 4445  df-suc 6040 This theorem is referenced by:  sucid  6113  nsuceq0  6114  trsuc  6118  sucssel  6126  ordsuc  7351  onpsssuc  7356  nlimsucg  7379  tfrlem11  7834  tfrlem13  7836  tz7.44-2  7853  omeulem1  8015  oeordi  8020  oeeulem  8034  php4  8506  wofib  8810  suc11reg  8882  cantnfle  8934  cantnflt2  8936  cantnfp1lem3  8943  cantnflem1  8952  dfac12lem1  9369  dfac12lem2  9370  ttukeylem3  9737  ttukeylem7  9741  r1wunlim  9963  fmla  32231  noresle  32761  noprefixmo  32763  ontgval  33339  sucneqond  34128  finxpreclem4  34156  finxpsuclem  34159
 Copyright terms: Public domain W3C validator