Theorem sucid 6401

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

Syntax hints:   ∈ wcel 2114  Vcvv 3430  suc csuc 6319

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-sn 4569  df-suc 6323

This theorem is referenced by:  eqelsuc  6403  unon  7775  onuninsuci  7784  tfinds  7804  peano5  7837  tfrlem16  8325  oawordeulem  8482  oalimcl  8488  omlimcl  8506  oneo  8509  omeulem1  8510  oeworde  8522  nnawordex  8566  nnneo  8584  naddcllem  8605  phplem2  9132  php  9134  fiint  9230  inf0  9533  oancom  9563  cantnfval2  9581  cantnflt  9584  cantnflem1  9601  cnfcom  9612  cnfcom2  9614  cnfcom3lem  9615  cnfcom3  9616  ssttrcl  9627  ttrcltr  9628  ttrclss  9632  rnttrcl  9634  ttrclselem2  9638  r1val1  9701  rankxplim3  9796  cardlim  9887  fseqenlem1  9937  cardaleph  10002  pwsdompw  10116  cfsmolem  10183  axdc3lem4  10366  ttukeylem5  10426  ttukeylem6  10427  ttukeylem7  10428  canthp1lem2  10567  pwxpndom2  10579  winainflem  10607  winalim2  10610  nqereu  10843  nogt01o  27674  bdayiun  27921  n0bday  28358  bnj216  34891  bnj98  35025  fineqvnttrclse  35284  satom  35554  fmla  35579  ex-sategoelel12  35625  dfrdg2  35991  preel  38835  dford3lem2  43473  pw2f1ocnv  43483  aomclem1  43500  nnoeomeqom  43758  naddgeoa  43840  naddwordnexlem4  43847