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

Theorem sucid 6267
 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 6266 . 2 (𝐴 ∈ V → 𝐴 ∈ suc 𝐴)
31, 2ax-mp 5 1 𝐴 ∈ suc 𝐴
 Colors of variables: wff setvar class Syntax hints:   ∈ wcel 2107  Vcvv 3499  suc csuc 6190 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-v 3501  df-un 3944  df-sn 4564  df-suc 6194 This theorem is referenced by:  eqelsuc  6269  unon  7537  onuninsuci  7546  tfinds  7565  peano5  7596  tfrlem16  8023  oawordeulem  8173  oalimcl  8179  omlimcl  8197  oneo  8200  omeulem1  8201  oeworde  8212  nnawordex  8256  nnneo  8271  phplem4  8691  php  8693  fiint  8787  inf0  9076  oancom  9106  cantnfval2  9124  cantnflt  9127  cantnflem1  9144  cnfcom  9155  cnfcom2  9157  cnfcom3lem  9158  cnfcom3  9159  r1val1  9207  rankxplim3  9302  cardlim  9393  fseqenlem1  9442  cardaleph  9507  pwsdompw  9618  cfsmolem  9684  axdc3lem4  9867  ttukeylem5  9927  ttukeylem6  9928  ttukeylem7  9929  canthp1lem2  10067  pwxpndom2  10079  winainflem  10107  winalim2  10110  nqereu  10343  bnj216  31891  bnj98  32028  satom  32490  fmla  32515  ex-sategoelel12  32561  dfrdg2  32927  dford3lem2  39492  pw2f1ocnv  39502  aomclem1  39522
 Copyright terms: Public domain W3C validator