Theorem sucid 6238

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

Syntax hints:   ∈ wcel 2111  Vcvv 3441  suc csuc 6161

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-suc 6165

This theorem is referenced by:  eqelsuc  6240  unon  7526  onuninsuci  7535  tfinds  7554  peano5  7585  tfrlem16  8012  oawordeulem  8163  oalimcl  8169  omlimcl  8187  oneo  8190  omeulem1  8191  oeworde  8202  nnawordex  8246  nnneo  8261  phplem4  8683  php  8685  fiint  8779  inf0  9068  oancom  9098  cantnfval2  9116  cantnflt  9119  cantnflem1  9136  cnfcom  9147  cnfcom2  9149  cnfcom3lem  9150  cnfcom3  9151  r1val1  9199  rankxplim3  9294  cardlim  9385  fseqenlem1  9435  cardaleph  9500  pwsdompw  9615  cfsmolem  9681  axdc3lem4  9864  ttukeylem5  9924  ttukeylem6  9925  ttukeylem7  9926  canthp1lem2  10064  pwxpndom2  10076  winainflem  10104  winalim2  10107  nqereu  10340  bnj216  32112  bnj98  32249  satom  32716  fmla  32741  ex-sategoelel12  32787  dfrdg2  33153  dford3lem2  39968  pw2f1ocnv  39978  aomclem1  39998