Theorem sucid 6262

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

Syntax hints:   ∈ wcel 2114  Vcvv 3400  suc csuc 6185

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-v 3402  df-un 3858  df-sn 4527  df-suc 6189

This theorem is referenced by:  eqelsuc  6264  unon  7578  onuninsuci  7587  tfinds  7606  peano5  7637  peano5OLD  7638  tfrlem16  8071  oawordeulem  8224  oalimcl  8230  omlimcl  8248  oneo  8251  omeulem1  8252  oeworde  8263  nnawordex  8307  nnneo  8322  phplem4  8762  php  8764  fiint  8882  inf0  9170  oancom  9200  cantnfval2  9218  cantnflt  9221  cantnflem1  9238  cnfcom  9249  cnfcom2  9251  cnfcom3lem  9252  cnfcom3  9253  r1val1  9301  rankxplim3  9396  cardlim  9487  fseqenlem1  9537  cardaleph  9602  pwsdompw  9717  cfsmolem  9783  axdc3lem4  9966  ttukeylem5  10026  ttukeylem6  10027  ttukeylem7  10028  canthp1lem2  10166  pwxpndom2  10178  winainflem  10206  winalim2  10209  nqereu  10442  bnj216  32294  bnj98  32431  satom  32902  fmla  32927  ex-sategoelel12  32973  dfrdg2  33358  naddcllem  33487  nogt01o  33555  dford3lem2  40462  pw2f1ocnv  40472  aomclem1  40492