Theorem sucid 6394

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

Syntax hints:   ∈ wcel 2119  Vcvv 3431  suc csuc 6312

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888  df-sn 4556  df-suc 6316

This theorem is referenced by:  eqelsuc  6396  unon  7771  onuninsuci  7780  tfinds  7800  peano5  7833  tfrlem16  8322  oawordeulem  8479  oalimcl  8485  omlimcl  8503  oneo  8506  omeulem1  8507  oeworde  8519  nnawordex  8563  nnneo  8581  naddcllem  8602  phplem2  9129  php  9131  fiint  9227  inf0  9533  oancom  9563  cantnfval2  9581  cantnflt  9584  cantnflem1  9601  cnfcom  9612  cnfcom2  9614  cnfcom3lem  9615  cnfcom3  9616  ssttrcl  9627  ttrcltr  9628  ttrclss  9632  rnttrcl  9634  ttrclselem2  9638  r1val1  9701  rankxplim3  9796  cardlim  9887  fseqenlem1  9937  cardaleph  10002  pwsdompw  10116  cfsmolem  10183  axdc3lem4  10366  ttukeylem5  10426  ttukeylem6  10427  ttukeylem7  10428  canthp1lem2  10567  pwxpndom2  10579  winainflem  10607  winalim2  10610  nqereu  10843  nogt01o  27678  bdayiun  27925  n0bday  28362  bnj216  34915  bnj98  35049  fineqvnttrclse  35305  satom  35584  fmla  35609  ex-sategoelel12  35655  dfrdg2  36021  preel  38867  dford3lem2  43472  pw2f1ocnv  43482  aomclem1  43499  nnoeomeqom  43757  naddgeoa  43839  naddwordnexlem4  43846