Theorem sucid 6444

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

Syntax hints:   ∈ wcel 2107  Vcvv 3475  suc csuc 6364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3953  df-sn 4629  df-suc 6368

This theorem is referenced by:  eqelsuc  6446  unon  7816  onuninsuci  7826  tfinds  7846  peano5  7881  peano5OLD  7882  tfrlem16  8390  oawordeulem  8551  oalimcl  8557  omlimcl  8575  oneo  8578  omeulem1  8579  oeworde  8590  nnawordex  8634  nnneo  8651  naddcllem  8672  phplem2  9205  php  9207  phplem4OLD  9217  phpOLD  9219  fiint  9321  inf0  9613  oancom  9643  cantnfval2  9661  cantnflt  9664  cantnflem1  9681  cnfcom  9692  cnfcom2  9694  cnfcom3lem  9695  cnfcom3  9696  ssttrcl  9707  ttrcltr  9708  ttrclss  9712  rnttrcl  9714  ttrclselem2  9718  r1val1  9778  rankxplim3  9873  cardlim  9964  fseqenlem1  10016  cardaleph  10081  pwsdompw  10196  cfsmolem  10262  axdc3lem4  10445  ttukeylem5  10505  ttukeylem6  10506  ttukeylem7  10507  canthp1lem2  10645  pwxpndom2  10657  winainflem  10685  winalim2  10688  nqereu  10921  nogt01o  27189  bnj216  33732  bnj98  33867  satom  34336  fmla  34361  ex-sategoelel12  34407  dfrdg2  34756  dford3lem2  41752  pw2f1ocnv  41762  aomclem1  41782  nnoeomeqom  42048  naddgeoa  42131  naddwordnexlem4  42138