Theorem sucid 6401

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

Syntax hints:   ∈ wcel 2113  Vcvv 3440  suc csuc 6319

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-sn 4581  df-suc 6323

This theorem is referenced by:  eqelsuc  6403  unon  7773  onuninsuci  7782  tfinds  7802  peano5  7835  tfrlem16  8324  oawordeulem  8481  oalimcl  8487  omlimcl  8505  oneo  8508  omeulem1  8509  oeworde  8521  nnawordex  8565  nnneo  8583  naddcllem  8604  phplem2  9129  php  9131  fiint  9227  inf0  9530  oancom  9560  cantnfval2  9578  cantnflt  9581  cantnflem1  9598  cnfcom  9609  cnfcom2  9611  cnfcom3lem  9612  cnfcom3  9613  ssttrcl  9624  ttrcltr  9625  ttrclss  9629  rnttrcl  9631  ttrclselem2  9635  r1val1  9698  rankxplim3  9793  cardlim  9884  fseqenlem1  9934  cardaleph  9999  pwsdompw  10113  cfsmolem  10180  axdc3lem4  10363  ttukeylem5  10423  ttukeylem6  10424  ttukeylem7  10425  canthp1lem2  10564  pwxpndom2  10576  winainflem  10604  winalim2  10607  nqereu  10840  nogt01o  27664  bdayiun  27911  n0bday  28348  bnj216  34888  bnj98  35023  fineqvnttrclse  35280  satom  35550  fmla  35575  ex-sategoelel12  35621  dfrdg2  35987  preel  38673  dford3lem2  43269  pw2f1ocnv  43279  aomclem1  43296  nnoeomeqom  43554  naddgeoa  43636  naddwordnexlem4  43643