Theorem sucid 6433

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

Syntax hints:   ∈ wcel 2107  Vcvv 3457  suc csuc 6352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3459  df-un 3929  df-sn 4600  df-suc 6356

This theorem is referenced by:  eqelsuc  6435  unon  7820  onuninsuci  7830  tfinds  7850  peano5  7884  tfrlem16  8402  oawordeulem  8561  oalimcl  8567  omlimcl  8585  oneo  8588  omeulem1  8589  oeworde  8600  nnawordex  8644  nnneo  8662  naddcllem  8683  phplem2  9214  php  9216  phpOLD  9226  fiint  9333  fiintOLD  9334  inf0  9628  oancom  9658  cantnfval2  9676  cantnflt  9679  cantnflem1  9696  cnfcom  9707  cnfcom2  9709  cnfcom3lem  9710  cnfcom3  9711  ssttrcl  9722  ttrcltr  9723  ttrclss  9727  rnttrcl  9729  ttrclselem2  9733  r1val1  9793  rankxplim3  9888  cardlim  9979  fseqenlem1  10031  cardaleph  10096  pwsdompw  10210  cfsmolem  10277  axdc3lem4  10460  ttukeylem5  10520  ttukeylem6  10521  ttukeylem7  10522  canthp1lem2  10660  pwxpndom2  10672  winainflem  10700  winalim2  10703  nqereu  10936  nogt01o  27646  n0sbday  28259  pw2bday  28323  bnj216  34692  bnj98  34827  satom  35307  fmla  35332  ex-sategoelel12  35378  dfrdg2  35742  dford3lem2  42983  pw2f1ocnv  42993  aomclem1  43010  nnoeomeqom  43268  naddgeoa  43350  naddwordnexlem4  43357