Theorem sucid 6467

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

Syntax hints:   ∈ wcel 2105  Vcvv 3477  suc csuc 6387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-un 3967  df-sn 4631  df-suc 6391

This theorem is referenced by:  eqelsuc  6469  unon  7850  onuninsuci  7860  tfinds  7880  peano5  7915  tfrlem16  8431  oawordeulem  8590  oalimcl  8596  omlimcl  8614  oneo  8617  omeulem1  8618  oeworde  8629  nnawordex  8673  nnneo  8691  naddcllem  8712  phplem2  9242  php  9244  phplem4OLD  9254  phpOLD  9256  fiint  9363  fiintOLD  9364  inf0  9658  oancom  9688  cantnfval2  9706  cantnflt  9709  cantnflem1  9726  cnfcom  9737  cnfcom2  9739  cnfcom3lem  9740  cnfcom3  9741  ssttrcl  9752  ttrcltr  9753  ttrclss  9757  rnttrcl  9759  ttrclselem2  9763  r1val1  9823  rankxplim3  9918  cardlim  10009  fseqenlem1  10061  cardaleph  10126  pwsdompw  10240  cfsmolem  10307  axdc3lem4  10490  ttukeylem5  10550  ttukeylem6  10551  ttukeylem7  10552  canthp1lem2  10690  pwxpndom2  10702  winainflem  10730  winalim2  10733  nqereu  10966  nogt01o  27755  n0sbday  28368  pw2bday  28432  bnj216  34724  bnj98  34859  satom  35340  fmla  35365  ex-sategoelel12  35411  dfrdg2  35776  dford3lem2  43015  pw2f1ocnv  43025  aomclem1  43042  nnoeomeqom  43301  naddgeoa  43383  naddwordnexlem4  43390