Theorem sucex 7784

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 7783	. 2 ⊢ (𝐴 ∈ V → suc 𝐴 ∈ V)
3	1, 2	ax-mp 5	1 ⊢ suc 𝐴 ∈ V

Syntax hints:   ∈ wcel 2141  Vcvv 3453  suc csuc 6343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5243  ax-pr 5387  ax-un 7713

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-un 3907  df-in 3909  df-ss 3919  df-sn 4580  df-pr 4582  df-uni 4863  df-suc 6347

This theorem is referenced by:  orduninsuc  7818  tfindsg  7836  tfinds2  7839  finds  7872  findsg  7873  finds2  7874  seqomlem1  8415  oasuc  8487  onasuc  8491  naddcllem  8640  infensuc  9121  inf0  9570  inf3lem1  9577  dfom3  9596  cantnflt  9621  cantnflem1  9638  cnfcom  9649  brttrcl2  9663  ssttrcl  9664  ttrcltr  9665  ttrclss  9669  ttrclselem2  9675  infxpenlem  9963  pwsdompw  10153  cfslb2n  10219  cfsmolem  10221  fin1a2lem12  10362  axdc4lem  10406  alephreg  10534  bnj986  35211  bnj1018g  35219  bnj1018  35220  rankfilimbi  35358  fineqvnttrclse  35381  satf  35664  dfon2lem7  36098  nmulprop  36501  rdgssun  37833  dford3lem2  43565