Theorem sucid 6447

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

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450  suc csuc 6364

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4151  df-sn 4585  df-suc 6368

This theorem is used by:  eqelsuc  6449  unon  7843  onuninsuci  7852  tfinds  7872  peano5  7906  tfrlem16  8405  oawordeulem  8566  oalimcl  8572  omlimcl  8590  oneo  8593  omeulem1  8594  oeworde  8606  nnawordex  8650  nnneo  8668  naddcllem  8689  phplem2  9224  php  9226  fiint  9322  inf0  9626  oancom  9656  cantnfval2  9674  cantnflt  9677  cantnflem1  9694  cnfcom  9705  cnfcom2  9707  cnfcom3lem  9708  cnfcom3  9709  ssttrcl  9720  ttrcltr  9721  ttrclss  9725  rnttrcl  9727  ttrclselem2  9731  r1val1  9797  rankxplim3  9902  cardlim  10057  fseqenlem1  10107  cardaleph  10172  pwsdompw  10285  cfsmolem  10352  axdc3lem4  10535  ttukeylem5  10595  ttukeylem6  10596  ttukeylem7  10597  canthp1lem2  10742  pwxpndom2  10754  winainflem  10782  winalim2  10785  nqereu  11018  nogt01o  28059  bdayiun  28307  n0bday  28744  bnj216  35410  bnj98  35544  fineqvnttrclse  35849  satom  36208  fmla  36233  ex-sategoelel12  36279  dfrdg2  36650  nmulprop  37032  preel  39526  dford3lem2  44128  pw2f1ocnv  44138  aomclem1  44150  nnoeomeqom  44408  naddgeoa  44490  naddwordnexlem4  44497  parswapprop  50871