Theorem sucid 6442

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3450  suc csuc 6359

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 2732

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 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-sn 4585  df-suc 6363

This theorem is used by:  eqelsuc  6444  unon  7827  onuninsuci  7836  tfinds  7856  peano5  7890  tfrlem16  8382  oawordeulem  8541  oalimcl  8547  omlimcl  8565  oneo  8568  omeulem1  8569  oeworde  8581  nnawordex  8625  nnneo  8643  naddcllem  8664  phplem2  9199  php  9201  fiint  9296  inf0  9600  oancom  9630  cantnfval2  9648  cantnflt  9651  cantnflem1  9668  cnfcom  9679  cnfcom2  9681  cnfcom3lem  9682  cnfcom3  9683  ssttrcl  9694  ttrcltr  9695  ttrclss  9699  rnttrcl  9701  ttrclselem2  9705  r1val1  9768  rankxplim3  9863  cardlim  9977  fseqenlem1  10027  cardaleph  10092  pwsdompw  10205  cfsmolem  10272  axdc3lem4  10455  ttukeylem5  10515  ttukeylem6  10516  ttukeylem7  10517  canthp1lem2  10662  pwxpndom2  10674  winainflem  10702  winalim2  10705  nqereu  10938  nogt01o  27932  bdayiun  28180  n0bday  28617  bnj216  35242  bnj98  35376  fineqvnttrclse  35650  satom  35935  fmla  35960  ex-sategoelel12  36006  dfrdg2  36372  nmulprop  36770  preel  39248  dford3lem2  43868  pw2f1ocnv  43878  aomclem1  43895  nnoeomeqom  44153  naddgeoa  44235  naddwordnexlem4  44242