Theorem sucex 7176

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

Syntax hints:   ∈ wcel 2139  Vcvv 3340  suc csuc 5886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pr 5055  ax-un 7114

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rex 3056  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-sn 4322  df-pr 4324  df-uni 4589  df-suc 5890

This theorem is referenced by:  orduninsuc  7208  tfindsg  7225  tfinds2  7228  finds  7257  findsg  7258  finds2  7259  seqomlem1  7714  oasuc  7773  onasuc  7777  infensuc  8303  phplem4  8307  php  8309  inf0  8691  inf3lem1  8698  dfom3  8717  cantnflt  8742  cantnflem1  8759  cnfcom  8770  infxpenlem  9026  pwsdompw  9218  ackbij1lem5  9238  cfslb2n  9282  cfsmolem  9284  fin1a2lem12  9425  axdc4lem  9469  alephreg  9596  bnj986  31331  bnj1018  31339  dfon2lem7  31999  bj-1ex  33244  bj-2ex  33245  cnfinltrel  33552  dford3lem2  38096