Theorem sucex 7785

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

Syntax hints:   ∈ wcel 2109  Vcvv 3450  suc csuc 6337

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-sn 4593  df-pr 4595  df-uni 4875  df-suc 6341

This theorem is referenced by:  orduninsuc  7822  tfindsg  7840  tfinds2  7843  finds  7875  findsg  7876  finds2  7877  seqomlem1  8421  oasuc  8491  onasuc  8495  naddcllem  8643  infensuc  9125  inf0  9581  inf3lem1  9588  dfom3  9607  cantnflt  9632  cantnflem1  9649  cnfcom  9660  brttrcl2  9674  ssttrcl  9675  ttrcltr  9676  ttrclss  9680  ttrclselem2  9686  infxpenlem  9973  pwsdompw  10163  cfslb2n  10228  cfsmolem  10230  fin1a2lem12  10371  axdc4lem  10415  alephreg  10542  bnj986  34952  bnj1018g  34960  bnj1018  34961  satf  35347  dfon2lem7  35784  rdgssun  37373  dford3lem2  43023