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

Theorem sucidg 6450
Description: Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized). Lemma 1.7 of [Schloeder] p. 1. (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 2728 . . 3 𝐴 = 𝐴
21olci 865 . 2 (𝐴𝐴𝐴 = 𝐴)
3 elsucg 6437 . 2 (𝐴𝑉 → (𝐴 ∈ suc 𝐴 ↔ (𝐴𝐴𝐴 = 𝐴)))
42, 3mpbiri 258 1 (𝐴𝑉𝐴 ∈ suc 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 846   = wceq 1534  wcel 2099  suc csuc 6371
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3473  df-un 3952  df-sn 4630  df-suc 6375
This theorem is referenced by:  sucid  6451  nsuceq0  6452  trsuc  6456  sucssel  6464  ordsuc  7816  ordsucOLD  7817  onpsssuc  7822  nlimsucg  7846  tfrlem11  8408  tfrlem13  8410  tz7.44-2  8427  omeulem1  8602  oeordi  8607  oeeulem  8621  dif1enlem  9180  dif1enlemOLD  9181  rexdif1en  9182  rexdif1enOLD  9183  dif1en  9184  dif1enOLD  9186  php4  9237  wofib  9568  suc11reg  9642  cantnfle  9694  cantnflt2  9696  cantnfp1lem3  9703  cantnflem1  9712  dfac12lem1  10166  dfac12lem2  10167  ttukeylem3  10534  ttukeylem7  10538  r1wunlim  10760  noresle  27629  nosupprefixmo  27632  noinfprefixmo  27633  fmla  34991  ex-sategoelelomsuc  35036  ontgval  35915  sucneqond  36844  finxpreclem4  36873  finxpsuclem  36876  onexgt  42668  onepsuc  42680  ordnexbtwnsuc  42696  nlimsuc  42871  sucomisnotcard  42974
  Copyright terms: Public domain W3C validator