Theorem sucid 6416

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

Syntax hints:   ∈ wcel 2109  Vcvv 3447  suc csuc 6334

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-sn 4590  df-suc 6338

This theorem is referenced by:  eqelsuc  6418  unon  7806  onuninsuci  7816  tfinds  7836  peano5  7869  tfrlem16  8361  oawordeulem  8518  oalimcl  8524  omlimcl  8542  oneo  8545  omeulem1  8546  oeworde  8557  nnawordex  8601  nnneo  8619  naddcllem  8640  phplem2  9169  php  9171  fiint  9277  fiintOLD  9278  inf0  9574  oancom  9604  cantnfval2  9622  cantnflt  9625  cantnflem1  9642  cnfcom  9653  cnfcom2  9655  cnfcom3lem  9656  cnfcom3  9657  ssttrcl  9668  ttrcltr  9669  ttrclss  9673  rnttrcl  9675  ttrclselem2  9679  r1val1  9739  rankxplim3  9834  cardlim  9925  fseqenlem1  9977  cardaleph  10042  pwsdompw  10156  cfsmolem  10223  axdc3lem4  10406  ttukeylem5  10466  ttukeylem6  10467  ttukeylem7  10468  canthp1lem2  10606  pwxpndom2  10618  winainflem  10646  winalim2  10649  nqereu  10882  nogt01o  27608  n0sbday  28244  bnj216  34722  bnj98  34857  satom  35343  fmla  35368  ex-sategoelel12  35414  dfrdg2  35783  dford3lem2  43016  pw2f1ocnv  43026  aomclem1  43043  nnoeomeqom  43301  naddgeoa  43383  naddwordnexlem4  43390