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

Theorem sucex 6640
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 6639 . 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 1767   _Vcvv 3118   suc csuc 4885
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4573  ax-nul 4581  ax-pr 4691  ax-un 6586
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-rex 2823  df-v 3120  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-sn 4033  df-pr 4035  df-uni 4251  df-suc 4889
This theorem is referenced by:  orduninsuc  6672  tfindsg  6689  tfinds2  6692  finds  6720  findsg  6721  finds2  6722  seqomlem1  7125  oasuc  7184  onasuc  7188  infensuc  7705  phplem4  7709  php  7711  inf0  8048  inf3lem1  8055  dfom3  8074  cantnflt  8101  cantnflem1  8118  cantnfltOLD  8131  cantnflem1OLD  8141  cnfcom  8154  cnfcomOLD  8162  infxpenlem  8401  pwsdompw  8594  ackbij1lem5  8614  cfslb2n  8658  cfsmolem  8660  fin1a2lem12  8801  axdc4lem  8845  alephreg  8967  dfon2lem7  29116  dford3lem2  30865  bnj986  33384  bnj1018  33392  bj-1ex  33881  bj-2ex  33882
  Copyright terms: Public domain W3C validator