Theorem sucex 7245

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

Syntax hints:   ∈ wcel 2157  Vcvv 3385  suc csuc 5943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777  ax-sep 4975  ax-nul 4983  ax-pr 5097  ax-un 7183

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-rex 3095  df-v 3387  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4116  df-sn 4369  df-pr 4371  df-uni 4629  df-suc 5947

This theorem is referenced by:  orduninsuc  7277  tfindsg  7294  tfinds2  7297  finds  7326  findsg  7327  finds2  7328  seqomlem1  7784  oasuc  7844  onasuc  7848  infensuc  8380  phplem4  8384  php  8386  inf0  8768  inf3lem1  8775  dfom3  8794  cantnflt  8819  cantnflem1  8836  cnfcom  8847  infxpenlem  9122  pwsdompw  9314  cfslb2n  9378  cfsmolem  9380  fin1a2lem12  9521  axdc4lem  9565  alephreg  9692  bnj986  31541  bnj1018  31549  dfon2lem7  32206  bj-2ex  33431  cnfinltrel  33739  dford3lem2  38375