Theorem sucex 7782

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

Syntax hints:   ∈ wcel 2109  Vcvv 3447  suc csuc 6334

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-sn 4590  df-pr 4592  df-uni 4872  df-suc 6338

This theorem is referenced by:  orduninsuc  7819  tfindsg  7837  tfinds2  7840  finds  7872  findsg  7873  finds2  7874  seqomlem1  8418  oasuc  8488  onasuc  8492  naddcllem  8640  infensuc  9119  inf0  9574  inf3lem1  9581  dfom3  9600  cantnflt  9625  cantnflem1  9642  cnfcom  9653  brttrcl2  9667  ssttrcl  9668  ttrcltr  9669  ttrclss  9673  ttrclselem2  9679  infxpenlem  9966  pwsdompw  10156  cfslb2n  10221  cfsmolem  10223  fin1a2lem12  10364  axdc4lem  10408  alephreg  10535  bnj986  34945  bnj1018g  34953  bnj1018  34954  satf  35340  dfon2lem7  35777  rdgssun  37366  dford3lem2  43016