Theorem sucex 7826

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

Syntax hints:   ∈ wcel 2108  Vcvv 3480  suc csuc 6386

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-sn 4627  df-pr 4629  df-uni 4908  df-suc 6390

This theorem is referenced by:  orduninsuc  7864  tfindsg  7882  tfinds2  7885  finds  7918  findsg  7919  finds2  7920  seqomlem1  8490  oasuc  8562  onasuc  8566  naddcllem  8714  infensuc  9195  phplem4OLD  9257  phpOLD  9259  inf0  9661  inf3lem1  9668  dfom3  9687  cantnflt  9712  cantnflem1  9729  cnfcom  9740  brttrcl2  9754  ssttrcl  9755  ttrcltr  9756  ttrclss  9760  ttrclselem2  9766  infxpenlem  10053  pwsdompw  10243  cfslb2n  10308  cfsmolem  10310  fin1a2lem12  10451  axdc4lem  10495  alephreg  10622  bnj986  34969  bnj1018g  34977  bnj1018  34978  satf  35358  dfon2lem7  35790  rdgssun  37379  dford3lem2  43039