Theorem sucid 6398

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

Syntax hints:   ∈ wcel 2113  Vcvv 3437  suc csuc 6316

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 2705

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 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-sn 4578  df-suc 6320

This theorem is referenced by:  eqelsuc  6400  unon  7770  onuninsuci  7779  tfinds  7799  peano5  7832  tfrlem16  8321  oawordeulem  8478  oalimcl  8484  omlimcl  8502  oneo  8505  omeulem1  8506  oeworde  8517  nnawordex  8561  nnneo  8579  naddcllem  8600  phplem2  9125  php  9127  fiint  9222  inf0  9522  oancom  9552  cantnfval2  9570  cantnflt  9573  cantnflem1  9590  cnfcom  9601  cnfcom2  9603  cnfcom3lem  9604  cnfcom3  9605  ssttrcl  9616  ttrcltr  9617  ttrclss  9621  rnttrcl  9623  ttrclselem2  9627  r1val1  9690  rankxplim3  9785  cardlim  9876  fseqenlem1  9926  cardaleph  9991  pwsdompw  10105  cfsmolem  10172  axdc3lem4  10355  ttukeylem5  10415  ttukeylem6  10416  ttukeylem7  10417  canthp1lem2  10555  pwxpndom2  10567  winainflem  10595  winalim2  10598  nqereu  10831  nogt01o  27655  bdayiun  27880  n0sbday  28300  bnj216  34816  bnj98  34951  fineqvnttrclse  35216  satom  35472  fmla  35497  ex-sategoelel12  35543  dfrdg2  35909  preel  38585  dford3lem2  43184  pw2f1ocnv  43194  aomclem1  43211  nnoeomeqom  43469  naddgeoa  43551  naddwordnexlem4  43558