Theorem sucid 5721

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

Syntax hints:   ∈ wcel 1977  Vcvv 3173  suc csuc 5642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-sn 4126  df-suc 5646

This theorem is referenced by:  eqelsuc  5723  unon  6923  onuninsuci  6932  tfinds  6951  peano5  6981  tfrlem16  7376  oawordeulem  7521  oalimcl  7527  omlimcl  7545  oneo  7548  omeulem1  7549  oeworde  7560  nnawordex  7604  nnneo  7618  phplem4  8027  php  8029  fiint  8122  inf0  8401  oancom  8431  cantnfval2  8449  cantnflt  8452  cantnflem1  8469  cnfcom  8480  cnfcom2  8482  cnfcom3lem  8483  cnfcom3  8484  r1val1  8532  rankxplim3  8627  cardlim  8681  fseqenlem1  8730  cardaleph  8795  pwsdompw  8909  cfsmolem  8975  axdc3lem4  9158  ttukeylem5  9218  ttukeylem6  9219  ttukeylem7  9220  canthp1lem2  9354  pwxpndom2  9366  winainflem  9394  winalim2  9397  nqereu  9630  bnj216  30054  bnj98  30191  dfrdg2  30945  nofulllem5  31105  dford3lem2  36612  pw2f1ocnv  36622  aomclem1  36642