Theorem sucid 6272

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

Syntax hints:   ∈ wcel 2114  Vcvv 3496  suc csuc 6195

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-un 3943  df-sn 4570  df-suc 6199

This theorem is referenced by:  eqelsuc  6274  unon  7548  onuninsuci  7557  tfinds  7576  peano5  7607  tfrlem16  8031  oawordeulem  8182  oalimcl  8188  omlimcl  8206  oneo  8209  omeulem1  8210  oeworde  8221  nnawordex  8265  nnneo  8280  phplem4  8701  php  8703  fiint  8797  inf0  9086  oancom  9116  cantnfval2  9134  cantnflt  9137  cantnflem1  9154  cnfcom  9165  cnfcom2  9167  cnfcom3lem  9168  cnfcom3  9169  r1val1  9217  rankxplim3  9312  cardlim  9403  fseqenlem1  9452  cardaleph  9517  pwsdompw  9628  cfsmolem  9694  axdc3lem4  9877  ttukeylem5  9937  ttukeylem6  9938  ttukeylem7  9939  canthp1lem2  10077  pwxpndom2  10089  winainflem  10117  winalim2  10120  nqereu  10353  bnj216  32004  bnj98  32141  satom  32605  fmla  32630  ex-sategoelel12  32676  dfrdg2  33042  dford3lem2  39631  pw2f1ocnv  39641  aomclem1  39661