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

Theorem sucex 7176
Description: The successor of a set is a set. (Contributed by NM, 30-Aug-1993.)
Hypothesis
Ref Expression
sucex.1 𝐴 ∈ V
Assertion
Ref Expression
sucex suc 𝐴 ∈ V

Proof of Theorem sucex
StepHypRef Expression
1 sucex.1 . 2 𝐴 ∈ V
2 sucexg 7175 . 2 (𝐴 ∈ V → suc 𝐴 ∈ V)
31, 2ax-mp 5 1 suc 𝐴 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2139  Vcvv 3340  suc csuc 5886
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pr 5055  ax-un 7114
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rex 3056  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-sn 4322  df-pr 4324  df-uni 4589  df-suc 5890
This theorem is referenced by:  orduninsuc  7208  tfindsg  7225  tfinds2  7228  finds  7257  findsg  7258  finds2  7259  seqomlem1  7714  oasuc  7773  onasuc  7777  infensuc  8303  phplem4  8307  php  8309  inf0  8691  inf3lem1  8698  dfom3  8717  cantnflt  8742  cantnflem1  8759  cnfcom  8770  infxpenlem  9026  pwsdompw  9218  ackbij1lem5  9238  cfslb2n  9282  cfsmolem  9284  fin1a2lem12  9425  axdc4lem  9469  alephreg  9596  bnj986  31331  bnj1018  31339  dfon2lem7  31999  bj-1ex  33244  bj-2ex  33245  cnfinltrel  33552  dford3lem2  38096
  Copyright terms: Public domain W3C validator