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

Theorem elelsuc 6459
Description: Membership in a successor. (Contributed by NM, 20-Jun-1998.)
Assertion
Ref Expression
elelsuc (𝐴𝐵𝐴 ∈ suc 𝐵)

Proof of Theorem elelsuc
StepHypRef Expression
1 orc 867 . 2 (𝐴𝐵 → (𝐴𝐵𝐴 = 𝐵))
2 elsucg 6454 . 2 (𝐴𝐵 → (𝐴 ∈ suc 𝐵 ↔ (𝐴𝐵𝐴 = 𝐵)))
31, 2mpbird 257 1 (𝐴𝐵𝐴 ∈ suc 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 847   = wceq 1537  wcel 2106  suc csuc 6388
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968  df-sn 4632  df-suc 6392
This theorem is referenced by:  suctr  6472  pssnn  9207  ttrcltr  9754  ttrclss  9758  ttrclselem2  9764  pwsdompw  10241  fin1a2lem4  10441  grur1a  10857  bnj570  34898  satom  35341  satfv0  35343  satfvsuc  35346  satf00  35359  satf0suc  35361  sat1el2xp  35364  fmla  35366  fmla0  35367  fmlasuc0  35369  satfdmfmla  35385  finxpsuclem  37380
  Copyright terms: Public domain W3C validator