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

Theorem sucex 6411
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 6410 . 2  |-  ( A  e.  _V  ->  suc  A  e.  _V )
31, 2ax-mp 5 1  |-  suc  A  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1755   _Vcvv 2962   suc csuc 4708
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519  ax-un 6361
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-rex 2711  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-sn 3866  df-pr 3868  df-uni 4080  df-suc 4712
This theorem is referenced by:  orduninsuc  6443  tfindsg  6460  tfinds2  6463  finds  6491  findsg  6492  finds2  6493  seqomlem1  6891  oasuc  6952  onasuc  6956  infensuc  7477  phplem4  7481  php  7483  inf0  7815  inf3lem1  7822  dfom3  7841  cantnflt  7868  cantnflem1  7885  cantnfltOLD  7898  cantnflem1OLD  7908  cnfcom  7921  cnfcomOLD  7929  infxpenlem  8168  pwsdompw  8361  ackbij1lem5  8381  cfslb2n  8425  cfsmolem  8427  fin1a2lem12  8568  axdc4lem  8612  alephreg  8734  dfon2lem7  27449  dford3lem2  29221  bnj986  31649  bnj1018  31657  bj-1ex  32025  bj-2ex  32026
  Copyright terms: Public domain W3C validator