Theorem sucex 7811

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

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3457  suc csuc 6366

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 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406  ax-un 7742

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 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-un 3911  df-in 3913  df-ss 3923  df-sn 4592  df-pr 4594  df-uni 4875  df-suc 6370

This theorem is used by:  orduninsuc  7845  tfindsg  7863  tfinds2  7866  finds  7899  findsg  7900  finds2  7901  seqomlem1  8443  oasuc  8515  onasuc  8519  naddcllem  8668  infensuc  9150  inf0  9597  inf3lem1  9604  dfom3  9623  cantnflt  9648  cantnflem1  9665  cnfcom  9676  brttrcl2  9690  ssttrcl  9691  ttrcltr  9692  ttrclss  9696  ttrclselem2  9702  infxpenlem  10013  pwsdompw  10202  cfslb2n  10267  cfsmolem  10269  fin1a2lem12  10410  axdc4lem  10454  alephreg  10582  bnj986  35408  bnj1018g  35416  bnj1018  35417  rankfilimbi  35553  fineqvnttrclse  35594  satf  35882  dfon2lem7  36316  nmulprop  36719  rdgssun  38081  dford3lem2  43812