Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  sucid GIF version

Theorem sucid 4307
 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 4306 . 2 (𝐴 ∈ V → 𝐴 ∈ suc 𝐴)
31, 2ax-mp 5 1 𝐴 ∈ suc 𝐴
 Colors of variables: wff set class Syntax hints:   ∈ wcel 1463  Vcvv 2658  suc csuc 4255 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097 This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-v 2660  df-un 3043  df-sn 3501  df-suc 4261 This theorem is referenced by:  eqelsuc  4309  unon  4395  ordunisuc2r  4398  ordsoexmid  4445  limom  4495  0elnn  4500  tfrexlem  6197  tfri1dALT  6214  tfrcl  6227  frecabcl  6262  phplem4  6715  fiintim  6783  fidcenumlemr  6809  infnninf  6988  nnnninf  6989  prarloclemarch2  7191  prarloclemlt  7265  ennnfonelemex  11833  ennnfonelemrn  11838  bj-nn0suc0  12982  bj-nnelirr  12985  bj-inf2vnlem2  13003  bj-findis  13011  nninfsellemeq  13044
 Copyright terms: Public domain W3C validator