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 2113  Vcvv 3438  suc csuc 6317

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375  ax-un 7678

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-sn 4579  df-pr 4581  df-uni 4862  df-suc 6321

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  9081  inf0  9528  inf3lem1  9535  dfom3  9554  cantnflt  9579  cantnflem1  9596  cnfcom  9607  brttrcl2  9621  ssttrcl  9622  ttrcltr  9623  ttrclss  9627  ttrclselem2  9633  infxpenlem  9921  pwsdompw  10111  cfslb2n  10176  cfsmolem  10178  fin1a2lem12  10319  axdc4lem  10363  alephreg  10491  bnj986  35060  bnj1018g  35068  bnj1018  35069  rankfilimbi  35206  fineqvnttrclse  35229  satf  35496  dfon2lem7  35930  rdgssun  37522  dford3lem2  43211