Theorem sucid 6447

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

Syntax hints:   ∈ wcel 2143  Vcvv 3455  suc csuc 6364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-sn 4591  df-suc 6368

This theorem is referenced by:  eqelsuc  6449  unon  7828  onuninsuci  7837  tfinds  7857  peano5  7891  tfrlem16  8381  oawordeulem  8540  oalimcl  8546  omlimcl  8564  oneo  8567  omeulem1  8568  oeworde  8580  nnawordex  8624  nnneo  8642  naddcllem  8663  phplem2  9190  php  9192  fiint  9287  inf0  9591  oancom  9621  cantnfval2  9639  cantnflt  9642  cantnflem1  9659  cnfcom  9670  cnfcom2  9672  cnfcom3lem  9673  cnfcom3  9674  ssttrcl  9685  ttrcltr  9686  ttrclss  9690  rnttrcl  9692  ttrclselem2  9696  r1val1  9759  rankxplim3  9854  cardlim  9959  fseqenlem1  10009  cardaleph  10074  pwsdompw  10187  cfsmolem  10255  axdc3lem4  10438  ttukeylem5  10498  ttukeylem6  10499  ttukeylem7  10500  canthp1lem2  10639  pwxpndom2  10651  winainflem  10679  winalim2  10682  nqereu  10915  nogt01o  27841  bdayiun  28089  n0bday  28526  bnj216  35102  bnj98  35236  fineqvnttrclse  35518  satom  35829  fmla  35854  ex-sategoelel12  35900  dfrdg2  36266  nmulprop  36663  preel  39130  dford3lem2  43737  pw2f1ocnv  43747  aomclem1  43764  nnoeomeqom  44022  naddgeoa  44104  naddwordnexlem4  44111