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

Theorem sucid 4652
 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
Assertion
Ref Expression
sucid

Proof of Theorem sucid
StepHypRef Expression
1 sucid.1 . 2
2 sucidg 4651 . 2
31, 2ax-mp 8 1
 Colors of variables: wff set class Syntax hints:   wcel 1725  cvv 2948   csuc 4575 This theorem is referenced by:  eqelsuc  4654  unon  4803  onuninsuci  4812  tfinds  4831  peano5  4860  tfrlem16  6646  oawordeulem  6789  oalimcl  6795  omlimcl  6813  oneo  6816  omeulem1  6817  oeworde  6828  nnawordex  6872  nnneo  6886  phplem4  7281  php  7283  fiint  7375  inf0  7568  oancom  7598  cantnfval2  7616  cantnflt  7619  cantnflem1  7637  cnfcom  7649  cnfcom2  7651  cnfcom3lem  7652  cnfcom3  7653  r1val1  7704  rankxplim3  7797  cardlim  7851  fseqenlem1  7897  cardaleph  7962  pwsdompw  8076  cfsmolem  8142  axdc3lem4  8325  ttukeylem5  8385  ttukeylem6  8386  ttukeylem7  8387  canthp1lem2  8520  pwxpndom2  8532  winainflem  8560  winalim2  8563  nqereu  8798  dfrdg2  25415  nofulllem5  25653  dford3lem2  27089  pw2f1ocnv  27099  aomclem1  27120  bnj216  29036  bnj98  29175 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-un 3317  df-sn 3812  df-suc 4579
 Copyright terms: Public domain W3C validator