Theorem sucex 7523

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

Syntax hints:   ∈ wcel 2112  Vcvv 3410  suc csuc 6169

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730  ax-sep 5167  ax-nul 5174  ax-pr 5296  ax-un 7457

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-tru 1542  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-rab 3080  df-v 3412  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-nul 4227  df-sn 4521  df-pr 4523  df-uni 4797  df-suc 6173

This theorem is referenced by:  orduninsuc  7555  tfindsg  7572  tfinds2  7575  finds  7606  findsg  7607  finds2  7608  seqomlem1  8094  2oex  8120  oasuc  8157  onasuc  8161  infensuc  8714  phplem4  8718  php  8720  inf0  9107  inf3lem1  9114  dfom3  9133  cantnflt  9158  cantnflem1  9175  cnfcom  9186  infxpenlem  9463  pwsdompw  9654  cfslb2n  9718  cfsmolem  9720  fin1a2lem12  9861  axdc4lem  9905  alephreg  10032  bnj986  32445  bnj1018g  32453  bnj1018  32454  satf  32821  dfon2lem7  33271  rdgssun  35065  dford3lem2  40331