Theorem sucex 7742

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

Syntax hints:   ∈ wcel 2109  Vcvv 3436  suc csuc 6309

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 5235  ax-nul 5245  ax-pr 5371  ax-un 7671

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-sn 4578  df-pr 4580  df-uni 4859  df-suc 6313

This theorem is referenced by:  orduninsuc  7776  tfindsg  7794  tfinds2  7797  finds  7829  findsg  7830  finds2  7831  seqomlem1  8372  oasuc  8442  onasuc  8446  naddcllem  8594  infensuc  9072  inf0  9517  inf3lem1  9524  dfom3  9543  cantnflt  9568  cantnflem1  9585  cnfcom  9596  brttrcl2  9610  ssttrcl  9611  ttrcltr  9612  ttrclss  9616  ttrclselem2  9622  infxpenlem  9907  pwsdompw  10097  cfslb2n  10162  cfsmolem  10164  fin1a2lem12  10305  axdc4lem  10349  alephreg  10476  bnj986  34922  bnj1018g  34930  bnj1018  34931  satf  35326  dfon2lem7  35763  rdgssun  37352  dford3lem2  43000