Theorem sucex 7751

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

Syntax hints:   ∈ wcel 2113  Vcvv 3440  suc csuc 6319

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-sn 4581  df-pr 4583  df-uni 4864  df-suc 6323

This theorem is referenced by:  orduninsuc  7785  tfindsg  7803  tfinds2  7806  finds  7838  findsg  7839  finds2  7840  seqomlem1  8381  oasuc  8451  onasuc  8455  naddcllem  8604  infensuc  9083  inf0  9530  inf3lem1  9537  dfom3  9556  cantnflt  9581  cantnflem1  9598  cnfcom  9609  brttrcl2  9623  ssttrcl  9624  ttrcltr  9625  ttrclss  9629  ttrclselem2  9635  infxpenlem  9923  pwsdompw  10113  cfslb2n  10178  cfsmolem  10180  fin1a2lem12  10321  axdc4lem  10365  alephreg  10493  bnj986  35111  bnj1018g  35119  bnj1018  35120  rankfilimbi  35257  fineqvnttrclse  35280  satf  35547  dfon2lem7  35981  rdgssun  37583  dford3lem2  43269