Theorem sucex 7506

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

Syntax hints:   ∈ wcel 2111  Vcvv 3441  suc csuc 6161

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-sn 4526  df-pr 4528  df-uni 4801  df-suc 6165

This theorem is referenced by:  orduninsuc  7538  tfindsg  7555  tfinds2  7558  finds  7589  findsg  7590  finds2  7591  seqomlem1  8069  2oex  8095  oasuc  8132  onasuc  8136  infensuc  8679  phplem4  8683  php  8685  inf0  9068  inf3lem1  9075  dfom3  9094  cantnflt  9119  cantnflem1  9136  cnfcom  9147  infxpenlem  9424  pwsdompw  9615  cfslb2n  9679  cfsmolem  9681  fin1a2lem12  9822  axdc4lem  9866  alephreg  9993  bnj986  32337  bnj1018g  32345  bnj1018  32346  satf  32713  dfon2lem7  33147  rdgssun  34795  dford3lem2  39968