Theorem sucid 6447

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

Syntax hints:   ∈ wcel 2104  Vcvv 3472  suc csuc 6367

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-un 3954  df-sn 4630  df-suc 6371

This theorem is referenced by:  eqelsuc  6449  unon  7823  onuninsuci  7833  tfinds  7853  peano5  7888  peano5OLD  7889  tfrlem16  8397  oawordeulem  8558  oalimcl  8564  omlimcl  8582  oneo  8585  omeulem1  8586  oeworde  8597  nnawordex  8641  nnneo  8658  naddcllem  8679  phplem2  9212  php  9214  phplem4OLD  9224  phpOLD  9226  fiint  9328  inf0  9620  oancom  9650  cantnfval2  9668  cantnflt  9671  cantnflem1  9688  cnfcom  9699  cnfcom2  9701  cnfcom3lem  9702  cnfcom3  9703  ssttrcl  9714  ttrcltr  9715  ttrclss  9719  rnttrcl  9721  ttrclselem2  9725  r1val1  9785  rankxplim3  9880  cardlim  9971  fseqenlem1  10023  cardaleph  10088  pwsdompw  10203  cfsmolem  10269  axdc3lem4  10452  ttukeylem5  10512  ttukeylem6  10513  ttukeylem7  10514  canthp1lem2  10652  pwxpndom2  10664  winainflem  10692  winalim2  10695  nqereu  10928  nogt01o  27433  bnj216  34039  bnj98  34174  satom  34643  fmla  34668  ex-sategoelel12  34714  dfrdg2  35069  dford3lem2  42070  pw2f1ocnv  42080  aomclem1  42100  nnoeomeqom  42366  naddgeoa  42449  naddwordnexlem4  42456