Theorem sucid 6419

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

Syntax hints:   ∈ wcel 2109  Vcvv 3450  suc csuc 6337

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-sn 4593  df-suc 6341

This theorem is referenced by:  eqelsuc  6421  unon  7809  onuninsuci  7819  tfinds  7839  peano5  7872  tfrlem16  8364  oawordeulem  8521  oalimcl  8527  omlimcl  8545  oneo  8548  omeulem1  8549  oeworde  8560  nnawordex  8604  nnneo  8622  naddcllem  8643  phplem2  9175  php  9177  fiint  9284  fiintOLD  9285  inf0  9581  oancom  9611  cantnfval2  9629  cantnflt  9632  cantnflem1  9649  cnfcom  9660  cnfcom2  9662  cnfcom3lem  9663  cnfcom3  9664  ssttrcl  9675  ttrcltr  9676  ttrclss  9680  rnttrcl  9682  ttrclselem2  9686  r1val1  9746  rankxplim3  9841  cardlim  9932  fseqenlem1  9984  cardaleph  10049  pwsdompw  10163  cfsmolem  10230  axdc3lem4  10413  ttukeylem5  10473  ttukeylem6  10474  ttukeylem7  10475  canthp1lem2  10613  pwxpndom2  10625  winainflem  10653  winalim2  10656  nqereu  10889  nogt01o  27615  n0sbday  28251  bnj216  34729  bnj98  34864  satom  35350  fmla  35375  ex-sategoelel12  35421  dfrdg2  35790  dford3lem2  43023  pw2f1ocnv  43033  aomclem1  43050  nnoeomeqom  43308  naddgeoa  43390  naddwordnexlem4  43397