Theorem sucex 7805

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3450  suc csuc 6359

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 2732  ax-sep 5251  ax-pr 5398  ax-un 7736

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-un 3904  df-in 3906  df-ss 3916  df-sn 4585  df-pr 4587  df-uni 4868  df-suc 6363

This theorem is used by:  orduninsuc  7839  tfindsg  7857  tfinds2  7860  finds  7893  findsg  7894  finds2  7895  seqomlem1  8439  oasuc  8511  onasuc  8515  naddcllem  8664  infensuc  9153  inf0  9600  inf3lem1  9607  dfom3  9626  cantnflt  9651  cantnflem1  9668  cnfcom  9679  brttrcl2  9693  ssttrcl  9694  ttrcltr  9695  ttrclss  9699  ttrclselem2  9705  infxpenlem  10016  pwsdompw  10205  cfslb2n  10270  cfsmolem  10272  fin1a2lem12  10413  axdc4lem  10457  alephreg  10591  bnj986  35464  bnj1018g  35472  bnj1018  35473  rankfilimbi  35609  fineqvnttrclse  35650  satf  35932  dfon2lem7  36366  nmulprop  36770  rdgssun  38132  dford3lem2  43868