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

Theorem sucid 5948
Description: A set belongs to its successor. (Contributed by NM, 22-Jun-1994.) (Proof shortened by Alan Sare, 18-Feb-2012.) (Proof shortened by Scott Fenton, 20-Feb-2012.)
Hypothesis
Ref Expression
sucid.1 𝐴 ∈ V
Assertion
Ref Expression
sucid 𝐴 ∈ suc 𝐴

Proof of Theorem sucid
StepHypRef Expression
1 sucid.1 . 2 𝐴 ∈ V
2 sucidg 5947 . 2 (𝐴 ∈ V → 𝐴 ∈ suc 𝐴)
31, 2ax-mp 5 1 𝐴 ∈ suc 𝐴
Colors of variables: wff setvar class
Syntax hints:  wcel 2145  Vcvv 3351  suc csuc 5869
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 829  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 3729  df-sn 4318  df-suc 5873
This theorem is referenced by:  eqelsuc  5950  unon  7179  onuninsuci  7188  tfinds  7207  peano5  7237  tfrlem16  7643  oawordeulem  7789  oalimcl  7795  omlimcl  7813  oneo  7816  omeulem1  7817  oeworde  7828  nnawordex  7872  nnneo  7886  phplem4  8299  php  8301  fiint  8394  inf0  8683  oancom  8713  cantnfval2  8731  cantnflt  8734  cantnflem1  8751  cnfcom  8762  cnfcom2  8764  cnfcom3lem  8765  cnfcom3  8766  r1val1  8814  rankxplim3  8909  cardlim  8999  fseqenlem1  9048  cardaleph  9113  pwsdompw  9229  cfsmolem  9295  axdc3lem4  9478  ttukeylem5  9538  ttukeylem6  9539  ttukeylem7  9540  canthp1lem2  9678  pwxpndom2  9690  winainflem  9718  winalim2  9721  nqereu  9954  bnj216  31139  bnj98  31276  dfrdg2  32038  dford3lem2  38121  pw2f1ocnv  38131  aomclem1  38151
  Copyright terms: Public domain W3C validator