Theorem sucid 6330

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

Syntax hints:   ∈ wcel 2108  Vcvv 3422  suc csuc 6253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-sn 4559  df-suc 6257

This theorem is referenced by:  eqelsuc  6332  unon  7653  onuninsuci  7662  tfinds  7681  peano5  7714  peano5OLD  7715  tfrlem16  8195  oawordeulem  8347  oalimcl  8353  omlimcl  8371  oneo  8374  omeulem1  8375  oeworde  8386  nnawordex  8430  nnneo  8445  phplem4  8895  php  8897  fiint  9021  inf0  9309  oancom  9339  cantnfval2  9357  cantnflt  9360  cantnflem1  9377  cnfcom  9388  cnfcom2  9390  cnfcom3lem  9391  cnfcom3  9392  r1val1  9475  rankxplim3  9570  cardlim  9661  fseqenlem1  9711  cardaleph  9776  pwsdompw  9891  cfsmolem  9957  axdc3lem4  10140  ttukeylem5  10200  ttukeylem6  10201  ttukeylem7  10202  canthp1lem2  10340  pwxpndom2  10352  winainflem  10380  winalim2  10383  nqereu  10616  bnj216  32611  bnj98  32747  satom  33218  fmla  33243  ex-sategoelel12  33289  dfrdg2  33677  ssttrcl  33701  ttrcltr  33702  ttrclss  33706  rnttrcl  33708  ttrclselem2  33712  naddcllem  33758  nogt01o  33826  dford3lem2  40765  pw2f1ocnv  40775  aomclem1  40795