Theorem sucid 6477

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

Syntax hints:   ∈ wcel 2108  Vcvv 3488  suc csuc 6397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-sn 4649  df-suc 6401

This theorem is referenced by:  eqelsuc  6479  unon  7867  onuninsuci  7877  tfinds  7897  peano5  7932  peano5OLD  7933  tfrlem16  8449  oawordeulem  8610  oalimcl  8616  omlimcl  8634  oneo  8637  omeulem1  8638  oeworde  8649  nnawordex  8693  nnneo  8711  naddcllem  8732  phplem2  9271  php  9273  phplem4OLD  9283  phpOLD  9285  fiint  9394  fiintOLD  9395  inf0  9690  oancom  9720  cantnfval2  9738  cantnflt  9741  cantnflem1  9758  cnfcom  9769  cnfcom2  9771  cnfcom3lem  9772  cnfcom3  9773  ssttrcl  9784  ttrcltr  9785  ttrclss  9789  rnttrcl  9791  ttrclselem2  9795  r1val1  9855  rankxplim3  9950  cardlim  10041  fseqenlem1  10093  cardaleph  10158  pwsdompw  10272  cfsmolem  10339  axdc3lem4  10522  ttukeylem5  10582  ttukeylem6  10583  ttukeylem7  10584  canthp1lem2  10722  pwxpndom2  10734  winainflem  10762  winalim2  10765  nqereu  10998  nogt01o  27759  n0sbday  28372  pw2bday  28436  bnj216  34708  bnj98  34843  satom  35324  fmla  35349  ex-sategoelel12  35395  dfrdg2  35759  dford3lem2  42984  pw2f1ocnv  42994  aomclem1  43011  nnoeomeqom  43274  naddgeoa  43356  naddwordnexlem4  43363