Theorem sucex 7854

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

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454  suc csuc 6390

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pr 5398  ax-un 7783

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-in 4094  df-un 4154  df-sn 4589  df-pr 4591  df-uni 4873  df-suc 6394

This theorem is used by:  orduninsuc  7888  tfindsg  7906  tfinds2  7909  finds  7942  findsg  7943  finds2  7944  seqomlem1  8498  oasuc  8570  onasuc  8574  naddcllem  8723  infensuc  9212  inf0  9659  inf3lem1  9666  dfom3  9685  cantnflt  9710  cantnflem1  9727  cnfcom  9738  brttrcl2  9752  ssttrcl  9753  ttrcltr  9754  ttrclss  9758  ttrclselem2  9764  rankfilimbi  9939  infxpenlem  10131  pwsdompw  10320  cfslb2n  10385  cfsmolem  10387  fin1a2lem12  10528  axdc4lem  10572  alephreg  10706  bnj986  35696  bnj1018g  35704  bnj1018  35705  fineqvnttrclse  35933  satf  36326  dfon2lem7  36766  nmulprop  37154  rdgssun  38569  dford3lem2  44300