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

Theorem sucidg 6396
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 2736 . . 3 𝐴 = 𝐴
21olci 864 . 2 (𝐴𝐴𝐴 = 𝐴)
3 elsucg 6383 . 2 (𝐴𝑉 → (𝐴 ∈ suc 𝐴 ↔ (𝐴𝐴𝐴 = 𝐴)))
42, 3mpbiri 257 1 (𝐴𝑉𝐴 ∈ suc 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 845   = wceq 1541  wcel 2106  suc csuc 6317
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3445  df-un 3913  df-sn 4585  df-suc 6321
This theorem is referenced by:  sucid  6397  nsuceq0  6398  trsuc  6402  sucssel  6410  ordsuc  7744  ordsucOLD  7745  onpsssuc  7750  nlimsucg  7774  tfrlem11  8330  tfrlem13  8332  tz7.44-2  8349  omeulem1  8525  oeordi  8530  oeeulem  8544  dif1enlem  9096  dif1enlemOLD  9097  rexdif1en  9098  rexdif1enOLD  9099  dif1en  9100  dif1enOLD  9102  php4  9153  wofib  9477  suc11reg  9551  cantnfle  9603  cantnflt2  9605  cantnfp1lem3  9612  cantnflem1  9621  dfac12lem1  10075  dfac12lem2  10076  ttukeylem3  10443  ttukeylem7  10447  r1wunlim  10669  noresle  27029  nosupprefixmo  27032  noinfprefixmo  27033  fmla  33844  ex-sategoelelomsuc  33889  ontgval  34870  sucneqond  35803  finxpreclem4  35832  finxpsuclem  35835  onexgt  41512  onepsuc  41524  ordnexbtwnsuc  41540  nlimsuc  41655  sucomisnotcard  41758
  Copyright terms: Public domain W3C validator