Theorem sucex 7749

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

Syntax hints:   ∈ wcel 2119  Vcvv 3431  suc csuc 6312

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-un 3888  df-in 3890  df-ss 3900  df-sn 4556  df-pr 4558  df-uni 4839  df-suc 6316

This theorem is referenced by:  orduninsuc  7783  tfindsg  7801  tfinds2  7804  finds  7836  findsg  7837  finds2  7838  seqomlem1  8379  oasuc  8449  onasuc  8453  naddcllem  8602  infensuc  9083  inf0  9533  inf3lem1  9540  dfom3  9559  cantnflt  9584  cantnflem1  9601  cnfcom  9612  brttrcl2  9626  ssttrcl  9627  ttrcltr  9628  ttrclss  9632  ttrclselem2  9638  infxpenlem  9926  pwsdompw  10116  cfslb2n  10181  cfsmolem  10183  fin1a2lem12  10324  axdc4lem  10368  alephreg  10496  bnj986  35137  bnj1018g  35145  bnj1018  35146  rankfilimbi  35282  fineqvnttrclse  35305  satf  35581  dfon2lem7  36015  rdgssun  37740  dford3lem2  43472