Theorem sucex 7633

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

Step	Hyp	Ref	Expression
1		sucex.1	. 2 ⊢ 𝐴 ∈ V
2		sucexg 7632	. 2 ⊢ (𝐴 ∈ V → suc 𝐴 ∈ V)
3	1, 2	ax-mp 5	1 ⊢ suc 𝐴 ∈ V

Syntax hints:   ∈ wcel 2108  Vcvv 3422  suc csuc 6253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-sn 4559  df-pr 4561  df-uni 4837  df-suc 6257

This theorem is referenced by:  orduninsuc  7665  tfindsg  7682  tfinds2  7685  finds  7719  findsg  7720  finds2  7721  seqomlem1  8251  2oexOLD  8285  oasuc  8316  onasuc  8320  infensuc  8891  phplem4  8895  php  8897  inf0  9309  inf3lem1  9316  dfom3  9335  cantnflt  9360  cantnflem1  9377  cnfcom  9388  infxpenlem  9700  pwsdompw  9891  cfslb2n  9955  cfsmolem  9957  fin1a2lem12  10098  axdc4lem  10142  alephreg  10269  bnj986  32835  bnj1018g  32843  bnj1018  32844  satf  33215  dfon2lem7  33671  brttrcl2  33700  ssttrcl  33701  ttrcltr  33702  ttrclss  33706  ttrclselem2  33712  naddcllem  33758  rdgssun  35476  dford3lem2  40765