Theorem sucid 6407

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

Syntax hints:   ∈ wcel 2114  Vcvv 3429  suc csuc 6325

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-sn 4568  df-suc 6329

This theorem is referenced by:  eqelsuc  6409  unon  7782  onuninsuci  7791  tfinds  7811  peano5  7844  tfrlem16  8332  oawordeulem  8489  oalimcl  8495  omlimcl  8513  oneo  8516  omeulem1  8517  oeworde  8529  nnawordex  8573  nnneo  8591  naddcllem  8612  phplem2  9139  php  9141  fiint  9237  inf0  9542  oancom  9572  cantnfval2  9590  cantnflt  9593  cantnflem1  9610  cnfcom  9621  cnfcom2  9623  cnfcom3lem  9624  cnfcom3  9625  ssttrcl  9636  ttrcltr  9637  ttrclss  9641  rnttrcl  9643  ttrclselem2  9647  r1val1  9710  rankxplim3  9805  cardlim  9896  fseqenlem1  9946  cardaleph  10011  pwsdompw  10125  cfsmolem  10192  axdc3lem4  10375  ttukeylem5  10435  ttukeylem6  10436  ttukeylem7  10437  canthp1lem2  10576  pwxpndom2  10588  winainflem  10616  winalim2  10619  nqereu  10852  nogt01o  27660  bdayiun  27907  n0bday  28344  bnj216  34875  bnj98  35009  fineqvnttrclse  35268  satom  35538  fmla  35563  ex-sategoelel12  35609  dfrdg2  35975  preel  38821  dford3lem2  43455  pw2f1ocnv  43465  aomclem1  43482  nnoeomeqom  43740  naddgeoa  43822  naddwordnexlem4  43829