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

Theorem sucex 4731
Description: The successor of a set is a set. (Contributed by NM, 30-Aug-1993.)
Hypothesis
Ref Expression
sucex.1  |-  A  e. 
_V
Assertion
Ref Expression
sucex  |-  suc  A  e.  _V

Proof of Theorem sucex
StepHypRef Expression
1 sucex.1 . 2  |-  A  e. 
_V
2 sucexg 4730 . 2  |-  ( A  e.  _V  ->  suc  A  e.  _V )
31, 2ax-mp 8 1  |-  suc  A  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1717   _Vcvv 2899   suc csuc 4524
This theorem is referenced by:  orduninsuc  4763  tfindsg  4780  tfinds2  4783  finds  4811  findsg  4812  finds2  4813  seqomlem1  6643  oasuc  6704  onasuc  6708  infensuc  7221  phplem4  7225  php  7227  inf0  7509  inf3lem1  7516  dfom3  7535  cantnflt  7560  cantnflem1  7578  cnfcom  7590  infxpenlem  7828  pwsdompw  8017  ackbij1lem5  8037  cfslb2n  8081  cfsmolem  8083  fin1a2lem12  8224  axdc4lem  8268  alephreg  8390  dfon2lem7  25169  dford3lem2  26789  bnj986  28663  bnj1018  28671
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-sep 4271  ax-nul 4279  ax-pr 4344  ax-un 4641
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-rex 2655  df-v 2901  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-sn 3763  df-pr 3764  df-uni 3958  df-suc 4528
  Copyright terms: Public domain W3C validator