Theorem sucid 6349

Description: A set belongs to its successor. (Contributed by NM, 22-Jun-1994.) (Proof shortened by Alan Sare, 18-Feb-2012.) (Proof shortened by Scott Fenton, 20-Feb-2012.)

Hypothesis

Ref	Expression
sucid.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
sucid	⊢ 𝐴 ∈ suc 𝐴

Proof of Theorem sucid

Step	Hyp	Ref	Expression
1		sucid.1	. 2 ⊢ 𝐴 ∈ V
2		sucidg 6348	. 2 ⊢ (𝐴 ∈ V → 𝐴 ∈ suc 𝐴)
3	1, 2	ax-mp 5	1 ⊢ 𝐴 ∈ suc 𝐴

Syntax hints:   ∈ wcel 2107  Vcvv 3433  suc csuc 6272

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-un 3893  df-sn 4563  df-suc 6276

This theorem is referenced by:  eqelsuc  6351  unon  7687  onuninsuci  7696  tfinds  7715  peano5  7749  peano5OLD  7750  tfrlem16  8233  oawordeulem  8394  oalimcl  8400  omlimcl  8418  oneo  8421  omeulem1  8422  oeworde  8433  nnawordex  8477  nnneo  8494  phplem2  9000  php  9002  phplem4OLD  9012  phpOLD  9014  fiint  9100  inf0  9388  oancom  9418  cantnfval2  9436  cantnflt  9439  cantnflem1  9456  cnfcom  9467  cnfcom2  9469  cnfcom3lem  9470  cnfcom3  9471  ssttrcl  9482  ttrcltr  9483  ttrclss  9487  rnttrcl  9489  ttrclselem2  9493  r1val1  9553  rankxplim3  9648  cardlim  9739  fseqenlem1  9789  cardaleph  9854  pwsdompw  9969  cfsmolem  10035  axdc3lem4  10218  ttukeylem5  10278  ttukeylem6  10279  ttukeylem7  10280  canthp1lem2  10418  pwxpndom2  10430  winainflem  10458  winalim2  10461  nqereu  10694  bnj216  32720  bnj98  32856  satom  33327  fmla  33352  ex-sategoelel12  33398  dfrdg2  33780  naddcllem  33840  nogt01o  33908  dford3lem2  40856  pw2f1ocnv  40866  aomclem1  40886