Theorem sucid 6446

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3451  suc csuc 6363

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-sn 4585  df-suc 6367

This theorem is used by:  eqelsuc  6448  unon  7840  onuninsuci  7849  tfinds  7869  peano5  7903  tfrlem16  8394  oawordeulem  8555  oalimcl  8561  omlimcl  8579  oneo  8582  omeulem1  8583  oeworde  8595  nnawordex  8639  nnneo  8657  naddcllem  8678  phplem2  9213  php  9215  fiint  9311  inf0  9615  oancom  9645  cantnfval2  9663  cantnflt  9666  cantnflem1  9683  cnfcom  9694  cnfcom2  9696  cnfcom3lem  9697  cnfcom3  9698  ssttrcl  9709  ttrcltr  9710  ttrclss  9714  rnttrcl  9716  ttrclselem2  9720  r1val1  9786  rankxplim3  9891  cardlim  10046  fseqenlem1  10096  cardaleph  10161  pwsdompw  10274  cfsmolem  10341  axdc3lem4  10524  ttukeylem5  10584  ttukeylem6  10585  ttukeylem7  10586  canthp1lem2  10731  pwxpndom2  10743  winainflem  10771  winalim2  10774  nqereu  11007  nogt01o  28046  bdayiun  28294  n0bday  28731  bnj216  35356  bnj98  35490  fineqvnttrclse  35775  satom  36100  fmla  36125  ex-sategoelel12  36171  dfrdg2  36537  nmulprop  36919  preel  39412  dford3lem2  44013  pw2f1ocnv  44023  aomclem1  44040  nnoeomeqom  44298  naddgeoa  44380  naddwordnexlem4  44387