Theorem sucid 6473

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

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454  suc csuc 6390

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154  df-sn 4589  df-suc 6394

This theorem is used by:  eqelsuc  6475  unon  7876  onuninsuci  7885  tfinds  7905  peano5  7939  tfrlem16  8439  oawordeulem  8600  oalimcl  8606  omlimcl  8624  oneo  8627  omeulem1  8628  oeworde  8640  nnawordex  8684  nnneo  8702  naddcllem  8723  phplem2  9258  php  9260  fiint  9356  inf0  9659  oancom  9689  cantnfval2  9707  cantnflt  9710  cantnflem1  9727  cnfcom  9738  cnfcom2  9740  cnfcom3lem  9741  cnfcom3  9742  ssttrcl  9753  ttrcltr  9754  ttrclss  9758  rnttrcl  9760  ttrclselem2  9764  r1val1  9830  rankxplim3  9935  cardlim  10090  fseqenlem1  10142  cardaleph  10207  pwsdompw  10320  cfsmolem  10387  axdc3lem4  10570  ttukeylem5  10630  ttukeylem6  10631  ttukeylem7  10632  canthp1lem2  10777  pwxpndom2  10789  winainflem  10817  winalim2  10820  nqereu  11053  nogt01o  28110  bdayiun  28358  n0bday  28795  bnj216  35474  bnj98  35608  fineqvnttrclse  35933  satom  36329  fmla  36354  ex-sategoelel12  36400  dfrdg2  36772  nmulprop  37154  preel  39698  dford3lem2  44300  pw2f1ocnv  44310  aomclem1  44322  nnoeomeqom  44575  naddgeoa  44657  naddwordnexlem4  44664  parswapprop  51108