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

Theorem sucid 4487
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 4486 . 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 1696   _Vcvv 2801   suc csuc 4410
This theorem is referenced by:  eqelsuc  4489  unon  4638  onuninsuci  4647  tfinds  4666  peano5  4695  tfrlem16  6425  oawordeulem  6568  oalimcl  6574  omlimcl  6592  oneo  6595  omeulem1  6596  oeworde  6607  nnawordex  6651  nnneo  6665  phplem4  7059  php  7061  fiint  7149  inf0  7338  oancom  7368  cantnfval2  7386  cantnflt  7389  cantnflem1  7407  cnfcom  7419  cnfcom2  7421  cnfcom3lem  7422  cnfcom3  7423  r1val1  7474  rankxplim3  7567  cardlim  7621  fseqenlem1  7667  cardaleph  7732  pwsdompw  7846  cfsmolem  7912  axdc3lem4  8095  ttukeylem5  8156  ttukeylem6  8157  ttukeylem7  8158  canthp1lem2  8291  pwxpndom2  8303  winainflem  8331  winalim2  8334  nqereu  8569  dfrdg2  24223  nofulllem5  24431  dford3lem2  27223  pw2f1ocnv  27233  aomclem1  27254  bnj216  29076  bnj98  29215
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-un 3170  df-sn 3659  df-suc 4414
  Copyright terms: Public domain W3C validator