Theorem sucid 6264

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

Syntax hints:   ∈ wcel 2110  Vcvv 3494  suc csuc 6187

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3940  df-sn 4561  df-suc 6191

This theorem is referenced by:  eqelsuc  6266  unon  7540  onuninsuci  7549  tfinds  7568  peano5  7599  tfrlem16  8023  oawordeulem  8174  oalimcl  8180  omlimcl  8198  oneo  8201  omeulem1  8202  oeworde  8213  nnawordex  8257  nnneo  8272  phplem4  8693  php  8695  fiint  8789  inf0  9078  oancom  9108  cantnfval2  9126  cantnflt  9129  cantnflem1  9146  cnfcom  9157  cnfcom2  9159  cnfcom3lem  9160  cnfcom3  9161  r1val1  9209  rankxplim3  9304  cardlim  9395  fseqenlem1  9444  cardaleph  9509  pwsdompw  9620  cfsmolem  9686  axdc3lem4  9869  ttukeylem5  9929  ttukeylem6  9930  ttukeylem7  9931  canthp1lem2  10069  pwxpndom2  10081  winainflem  10109  winalim2  10112  nqereu  10345  bnj216  31997  bnj98  32134  satom  32598  fmla  32623  ex-sategoelel12  32669  dfrdg2  33035  dford3lem2  39617  pw2f1ocnv  39627  aomclem1  39647