Theorem sucex 7746

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

Syntax hints:   ∈ wcel 2106  Vcvv 3446  suc csuc 6324

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 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389  ax-un 7677

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 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-sn 4592  df-pr 4594  df-uni 4871  df-suc 6328

This theorem is referenced by:  orduninsuc  7784  tfindsg  7802  tfinds2  7805  finds  7840  findsg  7841  finds2  7842  seqomlem1  8401  2oexOLD  8438  oasuc  8475  onasuc  8479  naddcllem  8627  infensuc  9106  phplem4OLD  9171  phpOLD  9173  inf0  9566  inf3lem1  9573  dfom3  9592  cantnflt  9617  cantnflem1  9634  cnfcom  9645  brttrcl2  9659  ssttrcl  9660  ttrcltr  9661  ttrclss  9665  ttrclselem2  9671  infxpenlem  9958  pwsdompw  10149  cfslb2n  10213  cfsmolem  10215  fin1a2lem12  10356  axdc4lem  10400  alephreg  10527  bnj986  33656  bnj1018g  33664  bnj1018  33665  satf  34034  dfon2lem7  34450  rdgssun  35922  dford3lem2  41409