Theorem sucid 6395

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

Syntax hints:   ∈ wcel 2109  Vcvv 3438  suc csuc 6313

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-un 3910  df-sn 4580  df-suc 6317

This theorem is referenced by:  eqelsuc  6397  unon  7770  onuninsuci  7780  tfinds  7800  peano5  7833  tfrlem16  8322  oawordeulem  8479  oalimcl  8485  omlimcl  8503  oneo  8506  omeulem1  8507  oeworde  8518  nnawordex  8562  nnneo  8580  naddcllem  8601  phplem2  9129  php  9131  fiint  9235  fiintOLD  9236  inf0  9536  oancom  9566  cantnfval2  9584  cantnflt  9587  cantnflem1  9604  cnfcom  9615  cnfcom2  9617  cnfcom3lem  9618  cnfcom3  9619  ssttrcl  9630  ttrcltr  9631  ttrclss  9635  rnttrcl  9637  ttrclselem2  9641  r1val1  9701  rankxplim3  9796  cardlim  9887  fseqenlem1  9937  cardaleph  10002  pwsdompw  10116  cfsmolem  10183  axdc3lem4  10366  ttukeylem5  10426  ttukeylem6  10427  ttukeylem7  10428  canthp1lem2  10566  pwxpndom2  10578  winainflem  10606  winalim2  10609  nqereu  10842  nogt01o  27624  bdayiun  27847  n0sbday  28267  bnj216  34701  bnj98  34836  satom  35331  fmla  35356  ex-sategoelel12  35402  dfrdg2  35771  dford3lem2  43003  pw2f1ocnv  43013  aomclem1  43030  nnoeomeqom  43288  naddgeoa  43370  naddwordnexlem4  43377