Theorem sucid 6409

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

Syntax hints:   ∈ wcel 2114  Vcvv 3442  suc csuc 6327

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 3444  df-un 3908  df-sn 4583  df-suc 6331

This theorem is referenced by:  eqelsuc  6411  unon  7783  onuninsuci  7792  tfinds  7812  peano5  7845  tfrlem16  8334  oawordeulem  8491  oalimcl  8497  omlimcl  8515  oneo  8518  omeulem1  8519  oeworde  8531  nnawordex  8575  nnneo  8593  naddcllem  8614  phplem2  9141  php  9143  fiint  9239  inf0  9542  oancom  9572  cantnfval2  9590  cantnflt  9593  cantnflem1  9610  cnfcom  9621  cnfcom2  9623  cnfcom3lem  9624  cnfcom3  9625  ssttrcl  9636  ttrcltr  9637  ttrclss  9641  rnttrcl  9643  ttrclselem2  9647  r1val1  9710  rankxplim3  9805  cardlim  9896  fseqenlem1  9946  cardaleph  10011  pwsdompw  10125  cfsmolem  10192  axdc3lem4  10375  ttukeylem5  10435  ttukeylem6  10436  ttukeylem7  10437  canthp1lem2  10576  pwxpndom2  10588  winainflem  10616  winalim2  10619  nqereu  10852  nogt01o  27676  bdayiun  27923  n0bday  28360  bnj216  34908  bnj98  35042  fineqvnttrclse  35299  satom  35569  fmla  35594  ex-sategoelel12  35640  dfrdg2  36006  preel  38748  dford3lem2  43381  pw2f1ocnv  43391  aomclem1  43408  nnoeomeqom  43666  naddgeoa  43748  naddwordnexlem4  43755