Theorem sucid 6442

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

Syntax hints:   ∈ wcel 2149  Vcvv 3463  suc csuc 6359

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-sn 4592  df-suc 6363

This theorem is referenced by:  eqelsuc  6444  unon  7823  onuninsuci  7832  tfinds  7852  peano5  7886  tfrlem16  8376  oawordeulem  8535  oalimcl  8541  omlimcl  8559  oneo  8562  omeulem1  8563  oeworde  8575  nnawordex  8619  nnneo  8637  naddcllem  8658  phplem2  9185  php  9187  fiint  9282  inf0  9586  oancom  9616  cantnfval2  9634  cantnflt  9637  cantnflem1  9654  cnfcom  9665  cnfcom2  9667  cnfcom3lem  9668  cnfcom3  9669  ssttrcl  9680  ttrcltr  9681  ttrclss  9685  rnttrcl  9687  ttrclselem2  9691  r1val1  9754  rankxplim3  9849  cardlim  9954  fseqenlem1  10004  cardaleph  10069  pwsdompw  10182  cfsmolem  10250  axdc3lem4  10433  ttukeylem5  10493  ttukeylem6  10494  ttukeylem7  10495  canthp1lem2  10634  pwxpndom2  10646  winainflem  10674  winalim2  10677  nqereu  10910  nogt01o  27822  bdayiun  28070  n0bday  28507  bnj216  35062  bnj98  35196  fineqvnttrclse  35456  satom  35743  fmla  35768  ex-sategoelel12  35814  dfrdg2  36180  nmulprop  36577  preel  39034  dford3lem2  43639  pw2f1ocnv  43649  aomclem1  43666  nnoeomeqom  43924  naddgeoa  44006  naddwordnexlem4  44013