Theorem sucex 7753

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

Syntax hints:   ∈ wcel 2114  Vcvv 3430  suc csuc 6319

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pr 5370  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-un 3895  df-in 3897  df-ss 3907  df-sn 4569  df-pr 4571  df-uni 4852  df-suc 6323

This theorem is referenced by:  orduninsuc  7787  tfindsg  7805  tfinds2  7808  finds  7840  findsg  7841  finds2  7842  seqomlem1  8382  oasuc  8452  onasuc  8456  naddcllem  8605  infensuc  9086  inf0  9533  inf3lem1  9540  dfom3  9559  cantnflt  9584  cantnflem1  9601  cnfcom  9612  brttrcl2  9626  ssttrcl  9627  ttrcltr  9628  ttrclss  9632  ttrclselem2  9638  infxpenlem  9926  pwsdompw  10116  cfslb2n  10181  cfsmolem  10183  fin1a2lem12  10324  axdc4lem  10368  alephreg  10496  bnj986  35113  bnj1018g  35121  bnj1018  35122  rankfilimbi  35260  fineqvnttrclse  35284  satf  35551  dfon2lem7  35985  rdgssun  37708  dford3lem2  43473