Theorem sucex 7801

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

Syntax hints:   ∈ wcel 2143  Vcvv 3455  suc csuc 6362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-un 3910  df-in 3912  df-ss 3922  df-sn 4590  df-pr 4592  df-uni 4873  df-suc 6366

This theorem is referenced by:  orduninsuc  7835  tfindsg  7853  tfinds2  7856  finds  7889  findsg  7890  finds2  7891  seqomlem1  8433  oasuc  8505  onasuc  8509  naddcllem  8658  infensuc  9139  inf0  9586  inf3lem1  9593  dfom3  9612  cantnflt  9637  cantnflem1  9654  cnfcom  9665  brttrcl2  9679  ssttrcl  9680  ttrcltr  9681  ttrclss  9685  ttrclselem2  9691  infxpenlem  9993  pwsdompw  10182  cfslb2n  10247  cfsmolem  10249  fin1a2lem12  10390  axdc4lem  10434  alephreg  10562  bnj986  35343  bnj1018g  35351  bnj1018  35352  rankfilimbi  35495  fineqvnttrclse  35537  satf  35845  dfon2lem7  36279  nmulprop  36682  rdgssun  38024  dford3lem2  43754