Theorem sucex 7818

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3451  suc csuc 6363

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391  ax-un 7749

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 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-un 3904  df-in 3906  df-ss 3916  df-sn 4585  df-pr 4587  df-uni 4868  df-suc 6367

This theorem is used by:  orduninsuc  7852  tfindsg  7870  tfinds2  7873  finds  7906  findsg  7907  finds2  7908  seqomlem1  8453  oasuc  8525  onasuc  8529  naddcllem  8678  infensuc  9167  inf0  9615  inf3lem1  9622  dfom3  9641  cantnflt  9666  cantnflem1  9683  cnfcom  9694  brttrcl2  9708  ssttrcl  9709  ttrcltr  9710  ttrclss  9714  ttrclselem2  9720  rankfilimbi  9895  infxpenlem  10085  pwsdompw  10274  cfslb2n  10339  cfsmolem  10341  fin1a2lem12  10482  axdc4lem  10526  alephreg  10660  bnj986  35578  bnj1018g  35586  bnj1018  35587  fineqvnttrclse  35775  satf  36097  dfon2lem7  36531  nmulprop  36919  rdgssun  38281  dford3lem2  44013