Theorem sucex 7804

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

Syntax hints:   ∈ wcel 2149  Vcvv 3463  suc csuc 6363

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-pr 5405  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-un 3918  df-in 3920  df-ss 3930  df-sn 4595  df-pr 4597  df-uni 4877  df-suc 6367

This theorem is referenced by:  orduninsuc  7838  tfindsg  7856  tfinds2  7859  finds  7892  findsg  7893  finds2  7894  seqomlem1  8436  oasuc  8508  onasuc  8512  naddcllem  8661  infensuc  9142  inf0  9589  inf3lem1  9596  dfom3  9615  cantnflt  9640  cantnflem1  9657  cnfcom  9668  brttrcl2  9682  ssttrcl  9683  ttrcltr  9684  ttrclss  9688  ttrclselem2  9694  infxpenlem  9996  pwsdompw  10185  cfslb2n  10251  cfsmolem  10253  fin1a2lem12  10394  axdc4lem  10438  alephreg  10566  bnj986  35287  bnj1018g  35295  bnj1018  35296  rankfilimbi  35436  fineqvnttrclse  35459  satf  35743  dfon2lem7  36177  nmulprop  36580  rdgssun  37911  dford3lem2  43645