MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sucid Structured version   Visualization version   GIF version

Theorem sucid 5763
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
StepHypRef Expression
1 sucid.1 . 2 𝐴 ∈ V
2 sucidg 5762 . 2 (𝐴 ∈ V → 𝐴 ∈ suc 𝐴)
31, 2ax-mp 5 1 𝐴 ∈ suc 𝐴
Colors of variables: wff setvar class
Syntax hints:  wcel 1987  Vcvv 3186  suc csuc 5684
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-un 3560  df-sn 4149  df-suc 5688
This theorem is referenced by:  eqelsuc  5765  unon  6978  onuninsuci  6987  tfinds  7006  peano5  7036  tfrlem16  7434  oawordeulem  7579  oalimcl  7585  omlimcl  7603  oneo  7606  omeulem1  7607  oeworde  7618  nnawordex  7662  nnneo  7676  phplem4  8086  php  8088  fiint  8181  inf0  8462  oancom  8492  cantnfval2  8510  cantnflt  8513  cantnflem1  8530  cnfcom  8541  cnfcom2  8543  cnfcom3lem  8544  cnfcom3  8545  r1val1  8593  rankxplim3  8688  cardlim  8742  fseqenlem1  8791  cardaleph  8856  pwsdompw  8970  cfsmolem  9036  axdc3lem4  9219  ttukeylem5  9279  ttukeylem6  9280  ttukeylem7  9281  canthp1lem2  9419  pwxpndom2  9431  winainflem  9459  winalim2  9462  nqereu  9695  bnj216  30508  bnj98  30645  dfrdg2  31402  dford3lem2  37074  pw2f1ocnv  37084  aomclem1  37104
  Copyright terms: Public domain W3C validator