Theorem sucid 6436

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

Syntax hints:   ∈ wcel 2098  Vcvv 3466  suc csuc 6356

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468  df-un 3945  df-sn 4621  df-suc 6360

This theorem is referenced by:  eqelsuc  6438  unon  7812  onuninsuci  7822  tfinds  7842  peano5  7877  peano5OLD  7878  tfrlem16  8388  oawordeulem  8549  oalimcl  8555  omlimcl  8573  oneo  8576  omeulem1  8577  oeworde  8588  nnawordex  8632  nnneo  8649  naddcllem  8670  phplem2  9203  php  9205  phplem4OLD  9215  phpOLD  9217  fiint  9319  inf0  9611  oancom  9641  cantnfval2  9659  cantnflt  9662  cantnflem1  9679  cnfcom  9690  cnfcom2  9692  cnfcom3lem  9693  cnfcom3  9694  ssttrcl  9705  ttrcltr  9706  ttrclss  9710  rnttrcl  9712  ttrclselem2  9716  r1val1  9776  rankxplim3  9871  cardlim  9962  fseqenlem1  10014  cardaleph  10079  pwsdompw  10194  cfsmolem  10260  axdc3lem4  10443  ttukeylem5  10503  ttukeylem6  10504  ttukeylem7  10505  canthp1lem2  10643  pwxpndom2  10655  winainflem  10683  winalim2  10686  nqereu  10919  nogt01o  27533  bnj216  34198  bnj98  34333  satom  34802  fmla  34827  ex-sategoelel12  34873  dfrdg2  35228  dford3lem2  42221  pw2f1ocnv  42231  aomclem1  42251  nnoeomeqom  42517  naddgeoa  42600  naddwordnexlem4  42607