Theorem sucex 7822

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

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450  suc csuc 6366

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390  ax-un 7753

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-in 4090  df-un 4150  df-sn 4585  df-pr 4587  df-uni 4867  df-suc 6370

This theorem is used by:  orduninsuc  7856  tfindsg  7874  tfinds2  7877  finds  7910  findsg  7911  finds2  7912  seqomlem1  8465  oasuc  8537  onasuc  8541  naddcllem  8690  infensuc  9179  inf0  9627  inf3lem1  9634  dfom3  9653  cantnflt  9678  cantnflem1  9695  cnfcom  9706  brttrcl2  9720  ssttrcl  9721  ttrcltr  9722  ttrclss  9726  ttrclselem2  9732  rankfilimbi  9907  infxpenlem  10097  pwsdompw  10286  cfslb2n  10351  cfsmolem  10353  fin1a2lem12  10494  axdc4lem  10538  alephreg  10672  bnj986  35633  bnj1018g  35641  bnj1018  35642  fineqvnttrclse  35850  satf  36206  dfon2lem7  36645  nmulprop  37033  rdgssun  38408  dford3lem2  44141