Theorem sucid 6466

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

Syntax hints:   ∈ wcel 2108  Vcvv 3480  suc csuc 6386

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-sn 4627  df-suc 6390

This theorem is referenced by:  eqelsuc  6468  unon  7851  onuninsuci  7861  tfinds  7881  peano5  7915  tfrlem16  8433  oawordeulem  8592  oalimcl  8598  omlimcl  8616  oneo  8619  omeulem1  8620  oeworde  8631  nnawordex  8675  nnneo  8693  naddcllem  8714  phplem2  9245  php  9247  phplem4OLD  9257  phpOLD  9259  fiint  9366  fiintOLD  9367  inf0  9661  oancom  9691  cantnfval2  9709  cantnflt  9712  cantnflem1  9729  cnfcom  9740  cnfcom2  9742  cnfcom3lem  9743  cnfcom3  9744  ssttrcl  9755  ttrcltr  9756  ttrclss  9760  rnttrcl  9762  ttrclselem2  9766  r1val1  9826  rankxplim3  9921  cardlim  10012  fseqenlem1  10064  cardaleph  10129  pwsdompw  10243  cfsmolem  10310  axdc3lem4  10493  ttukeylem5  10553  ttukeylem6  10554  ttukeylem7  10555  canthp1lem2  10693  pwxpndom2  10705  winainflem  10733  winalim2  10736  nqereu  10969  nogt01o  27741  n0sbday  28354  pw2bday  28418  bnj216  34746  bnj98  34881  satom  35361  fmla  35386  ex-sategoelel12  35432  dfrdg2  35796  dford3lem2  43039  pw2f1ocnv  43049  aomclem1  43066  nnoeomeqom  43325  naddgeoa  43407  naddwordnexlem4  43414