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

Theorem sucid 5989
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 5988 . 2 (𝐴 ∈ V → 𝐴 ∈ suc 𝐴)
31, 2ax-mp 5 1 𝐴 ∈ suc 𝐴
Colors of variables: wff setvar class
Syntax hints:  wcel 2155  Vcvv 3350  suc csuc 5912
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-v 3352  df-un 3739  df-sn 4337  df-suc 5916
This theorem is referenced by:  eqelsuc  5991  unon  7233  onuninsuci  7242  tfinds  7261  peano5  7291  tfrlem16  7697  oawordeulem  7843  oalimcl  7849  omlimcl  7867  oneo  7870  omeulem1  7871  oeworde  7882  nnawordex  7926  nnneo  7940  phplem4  8353  php  8355  fiint  8448  inf0  8737  oancom  8767  cantnfval2  8785  cantnflt  8788  cantnflem1  8805  cnfcom  8816  cnfcom2  8818  cnfcom3lem  8819  cnfcom3  8820  r1val1  8868  rankxplim3  8963  cardlim  9053  fseqenlem1  9102  cardaleph  9167  pwsdompw  9283  cfsmolem  9349  axdc3lem4  9532  ttukeylem5  9592  ttukeylem6  9593  ttukeylem7  9594  canthp1lem2  9732  pwxpndom2  9744  winainflem  9772  winalim2  9775  nqereu  10008  bnj216  31270  bnj98  31406  dfrdg2  32165  dford3lem2  38295  pw2f1ocnv  38305  aomclem1  38325
  Copyright terms: Public domain W3C validator