Theorem sucex 7842

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

Syntax hints:   ∈ wcel 2108  Vcvv 3488  suc csuc 6397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-sn 4649  df-pr 4651  df-uni 4932  df-suc 6401

This theorem is referenced by:  orduninsuc  7880  tfindsg  7898  tfinds2  7901  finds  7936  findsg  7937  finds2  7938  seqomlem1  8506  2oexOLD  8543  oasuc  8580  onasuc  8584  naddcllem  8732  infensuc  9221  phplem4OLD  9283  phpOLD  9285  inf0  9690  inf3lem1  9697  dfom3  9716  cantnflt  9741  cantnflem1  9758  cnfcom  9769  brttrcl2  9783  ssttrcl  9784  ttrcltr  9785  ttrclss  9789  ttrclselem2  9795  infxpenlem  10082  pwsdompw  10272  cfslb2n  10337  cfsmolem  10339  fin1a2lem12  10480  axdc4lem  10524  alephreg  10651  bnj986  34931  bnj1018g  34939  bnj1018  34940  satf  35321  dfon2lem7  35753  rdgssun  37344  dford3lem2  42984