Theorem sucex 7796

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

Syntax hints:   ∈ wcel 2106  Vcvv 3474  suc csuc 6366

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7727

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-sn 4629  df-pr 4631  df-uni 4909  df-suc 6370

This theorem is referenced by:  orduninsuc  7834  tfindsg  7852  tfinds2  7855  finds  7891  findsg  7892  finds2  7893  seqomlem1  8452  2oexOLD  8489  oasuc  8526  onasuc  8530  naddcllem  8677  infensuc  9157  phplem4OLD  9222  phpOLD  9224  inf0  9618  inf3lem1  9625  dfom3  9644  cantnflt  9669  cantnflem1  9686  cnfcom  9697  brttrcl2  9711  ssttrcl  9712  ttrcltr  9713  ttrclss  9717  ttrclselem2  9723  infxpenlem  10010  pwsdompw  10201  cfslb2n  10265  cfsmolem  10267  fin1a2lem12  10408  axdc4lem  10452  alephreg  10579  bnj986  34252  bnj1018g  34260  bnj1018  34261  satf  34630  dfon2lem7  35053  rdgssun  36562  dford3lem2  42068