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 2107  Vcvv 3475  suc csuc 6367

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 3954  df-sn 4630  df-suc 6371

This theorem is referenced by:  eqelsuc  6449  unon  7819  onuninsuci  7829  tfinds  7849  peano5  7884  peano5OLD  7885  tfrlem16  8393  oawordeulem  8554  oalimcl  8560  omlimcl  8578  oneo  8581  omeulem1  8582  oeworde  8593  nnawordex  8637  nnneo  8654  naddcllem  8675  phplem2  9208  php  9210  phplem4OLD  9220  phpOLD  9222  fiint  9324  inf0  9616  oancom  9646  cantnfval2  9664  cantnflt  9667  cantnflem1  9684  cnfcom  9695  cnfcom2  9697  cnfcom3lem  9698  cnfcom3  9699  ssttrcl  9710  ttrcltr  9711  ttrclss  9715  rnttrcl  9717  ttrclselem2  9721  r1val1  9781  rankxplim3  9876  cardlim  9967  fseqenlem1  10019  cardaleph  10084  pwsdompw  10199  cfsmolem  10265  axdc3lem4  10448  ttukeylem5  10508  ttukeylem6  10509  ttukeylem7  10510  canthp1lem2  10648  pwxpndom2  10660  winainflem  10688  winalim2  10691  nqereu  10924  nogt01o  27199  bnj216  33743  bnj98  33878  satom  34347  fmla  34372  ex-sategoelel12  34418  dfrdg2  34767  dford3lem2  41766  pw2f1ocnv  41776  aomclem1  41796  nnoeomeqom  42062  naddgeoa  42145  naddwordnexlem4  42152