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

Theorem sucid 4602
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  |-  A  e. 
_V
Assertion
Ref Expression
sucid  |-  A  e. 
suc  A

Proof of Theorem sucid
StepHypRef Expression
1 sucid.1 . 2  |-  A  e. 
_V
2 sucidg 4601 . 2  |-  ( A  e.  _V  ->  A  e.  suc  A )
31, 2ax-mp 8 1  |-  A  e. 
suc  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1717   _Vcvv 2900   suc csuc 4525
This theorem is referenced by:  eqelsuc  4604  unon  4752  onuninsuci  4761  tfinds  4780  peano5  4809  tfrlem16  6591  oawordeulem  6734  oalimcl  6740  omlimcl  6758  oneo  6761  omeulem1  6762  oeworde  6773  nnawordex  6817  nnneo  6831  phplem4  7226  php  7228  fiint  7320  inf0  7510  oancom  7540  cantnfval2  7558  cantnflt  7561  cantnflem1  7579  cnfcom  7591  cnfcom2  7593  cnfcom3lem  7594  cnfcom3  7595  r1val1  7646  rankxplim3  7739  cardlim  7793  fseqenlem1  7839  cardaleph  7904  pwsdompw  8018  cfsmolem  8084  axdc3lem4  8267  ttukeylem5  8327  ttukeylem6  8328  ttukeylem7  8329  canthp1lem2  8462  pwxpndom2  8474  winainflem  8502  winalim2  8505  nqereu  8740  dfrdg2  25177  nofulllem5  25385  dford3lem2  26790  pw2f1ocnv  26800  aomclem1  26821  bnj216  28438  bnj98  28577
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-v 2902  df-un 3269  df-sn 3764  df-suc 4529
  Copyright terms: Public domain W3C validator