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

Theorem sucid 4471
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  |-  A  e. 
_V
Assertion
Ref Expression
sucid  |-  A  e. 
suc  A

Proof of Theorem sucid
StepHypRef Expression
1 sucid.1 . 2  |-  A  e. 
_V
2 sucidg 4470 . 2  |-  ( A  e.  _V  ->  A  e.  suc  A )
31, 2ax-mp 8 1  |-  A  e. 
suc  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1684   _Vcvv 2788   suc csuc 4394
This theorem is referenced by:  eqelsuc  4473  unon  4622  onuninsuci  4631  tfinds  4650  peano5  4679  tfrlem16  6409  oawordeulem  6552  oalimcl  6558  omlimcl  6576  oneo  6579  omeulem1  6580  oeworde  6591  nnawordex  6635  nnneo  6649  phplem4  7043  php  7045  fiint  7133  inf0  7322  oancom  7352  cantnfval2  7370  cantnflt  7373  cantnflem1  7391  cnfcom  7403  cnfcom2  7405  cnfcom3lem  7406  cnfcom3  7407  r1val1  7458  rankxplim3  7551  cardlim  7605  fseqenlem1  7651  cardaleph  7716  pwsdompw  7830  cfsmolem  7896  axdc3lem4  8079  ttukeylem5  8140  ttukeylem6  8141  ttukeylem7  8142  canthp1lem2  8275  pwxpndom2  8287  winainflem  8315  winalim2  8318  nqereu  8553  dfrdg2  24152  nofulllem5  24360  dford3lem2  27120  pw2f1ocnv  27130  aomclem1  27151  bnj216  28760  bnj98  28899
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157  df-sn 3646  df-suc 4398
  Copyright terms: Public domain W3C validator