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

Theorem elelsuc 6456
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 6451 . 2 (𝐴𝐵 → (𝐴 ∈ suc 𝐵 ↔ (𝐴𝐵𝐴 = 𝐵)))
31, 2mpbird 257 1 (𝐴𝐵𝐴 ∈ suc 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 847   = wceq 1539  wcel 2107  suc csuc 6385
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-un 3955  df-sn 4626  df-suc 6389
This theorem is referenced by:  suctr  6469  pssnn  9209  ttrcltr  9757  ttrclss  9761  ttrclselem2  9767  pwsdompw  10244  fin1a2lem4  10444  grur1a  10860  bnj570  34920  satom  35362  satfv0  35364  satfvsuc  35367  satf00  35380  satf0suc  35382  sat1el2xp  35385  fmla  35387  fmla0  35388  fmlasuc0  35390  satfdmfmla  35406  finxpsuclem  37399
  Copyright terms: Public domain W3C validator