Theorem sucid 6436

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

Syntax hints:   ∈ wcel 2108  Vcvv 3459  suc csuc 6354

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-sn 4602  df-suc 6358

This theorem is referenced by:  eqelsuc  6438  unon  7825  onuninsuci  7835  tfinds  7855  peano5  7889  tfrlem16  8407  oawordeulem  8566  oalimcl  8572  omlimcl  8590  oneo  8593  omeulem1  8594  oeworde  8605  nnawordex  8649  nnneo  8667  naddcllem  8688  phplem2  9219  php  9221  phpOLD  9231  fiint  9338  fiintOLD  9339  inf0  9635  oancom  9665  cantnfval2  9683  cantnflt  9686  cantnflem1  9703  cnfcom  9714  cnfcom2  9716  cnfcom3lem  9717  cnfcom3  9718  ssttrcl  9729  ttrcltr  9730  ttrclss  9734  rnttrcl  9736  ttrclselem2  9740  r1val1  9800  rankxplim3  9895  cardlim  9986  fseqenlem1  10038  cardaleph  10103  pwsdompw  10217  cfsmolem  10284  axdc3lem4  10467  ttukeylem5  10527  ttukeylem6  10528  ttukeylem7  10529  canthp1lem2  10667  pwxpndom2  10679  winainflem  10707  winalim2  10710  nqereu  10943  nogt01o  27660  n0sbday  28296  bnj216  34763  bnj98  34898  satom  35378  fmla  35403  ex-sategoelel12  35449  dfrdg2  35813  dford3lem2  43051  pw2f1ocnv  43061  aomclem1  43078  nnoeomeqom  43336  naddgeoa  43418  naddwordnexlem4  43425