Theorem sucid 6449

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

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3457  suc csuc 6366

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-sn 4592  df-suc 6370

This theorem is used by:  eqelsuc  6451  unon  7829  onuninsuci  7838  tfinds  7858  peano5  7892  tfrlem16  8382  oawordeulem  8541  oalimcl  8547  omlimcl  8565  oneo  8568  omeulem1  8569  oeworde  8581  nnawordex  8625  nnneo  8643  naddcllem  8664  phplem2  9192  php  9194  fiint  9289  inf0  9593  oancom  9623  cantnfval2  9641  cantnflt  9644  cantnflem1  9661  cnfcom  9672  cnfcom2  9674  cnfcom3lem  9675  cnfcom3  9676  ssttrcl  9687  ttrcltr  9688  ttrclss  9692  rnttrcl  9694  ttrclselem2  9698  r1val1  9761  rankxplim3  9856  cardlim  9970  fseqenlem1  10020  cardaleph  10085  pwsdompw  10198  cfsmolem  10265  axdc3lem4  10448  ttukeylem5  10508  ttukeylem6  10509  ttukeylem7  10510  canthp1lem2  10649  pwxpndom2  10661  winainflem  10689  winalim2  10692  nqereu  10925  nogt01o  27891  bdayiun  28139  n0bday  28576  bnj216  35162  bnj98  35296  fineqvnttrclse  35570  satom  35861  fmla  35886  ex-sategoelel12  35932  dfrdg2  36298  nmulprop  36695  preel  39182  dford3lem2  43787  pw2f1ocnv  43797  aomclem1  43814  nnoeomeqom  44072  naddgeoa  44154  naddwordnexlem4  44161