Theorem sucid 5802

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

Syntax hints:   ∈ wcel 1989  Vcvv 3198  suc csuc 5723

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-v 3200  df-un 3577  df-sn 4176  df-suc 5727

This theorem is referenced by:  eqelsuc  5804  unon  7028  onuninsuci  7037  tfinds  7056  peano5  7086  tfrlem16  7486  oawordeulem  7631  oalimcl  7637  omlimcl  7655  oneo  7658  omeulem1  7659  oeworde  7670  nnawordex  7714  nnneo  7728  phplem4  8139  php  8141  fiint  8234  inf0  8515  oancom  8545  cantnfval2  8563  cantnflt  8566  cantnflem1  8583  cnfcom  8594  cnfcom2  8596  cnfcom3lem  8597  cnfcom3  8598  r1val1  8646  rankxplim3  8741  cardlim  8795  fseqenlem1  8844  cardaleph  8909  pwsdompw  9023  cfsmolem  9089  axdc3lem4  9272  ttukeylem5  9332  ttukeylem6  9333  ttukeylem7  9334  canthp1lem2  9472  pwxpndom2  9484  winainflem  9512  winalim2  9515  nqereu  9748  bnj216  30785  bnj98  30922  dfrdg2  31685  dford3lem2  37420  pw2f1ocnv  37430  aomclem1  37450