Theorem sucex 7762

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

Syntax hints:   ∈ wcel 2109  Vcvv 3444  suc csuc 6322

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 5246  ax-nul 5256  ax-pr 5382  ax-un 7691

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-sn 4586  df-pr 4588  df-uni 4868  df-suc 6326

This theorem is referenced by:  orduninsuc  7799  tfindsg  7817  tfinds2  7820  finds  7852  findsg  7853  finds2  7854  seqomlem1  8395  oasuc  8465  onasuc  8469  naddcllem  8617  infensuc  9096  inf0  9550  inf3lem1  9557  dfom3  9576  cantnflt  9601  cantnflem1  9618  cnfcom  9629  brttrcl2  9643  ssttrcl  9644  ttrcltr  9645  ttrclss  9649  ttrclselem2  9655  infxpenlem  9942  pwsdompw  10132  cfslb2n  10197  cfsmolem  10199  fin1a2lem12  10340  axdc4lem  10384  alephreg  10511  bnj986  34918  bnj1018g  34926  bnj1018  34927  satf  35313  dfon2lem7  35750  rdgssun  37339  dford3lem2  42989