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

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

Proof of Theorem elelsuc
StepHypRef Expression
1 orc 864 . 2 (𝐴𝐵 → (𝐴𝐵𝐴 = 𝐵))
2 elsucg 6227 . 2 (𝐴𝐵 → (𝐴 ∈ suc 𝐵 ↔ (𝐴𝐵𝐴 = 𝐵)))
31, 2mpbird 260 1 (𝐴𝐵𝐴 ∈ suc 𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ wo 844   = wceq 1538   ∈ wcel 2111  suc csuc 6162 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-suc 6166 This theorem is referenced by:  suctr  6243  pssnn  8723  pwsdompw  9618  fin1a2lem4  9817  grur1a  10233  bnj570  32302  satom  32731  satfv0  32733  satfvsuc  32736  satf00  32749  satf0suc  32751  sat1el2xp  32754  fmla  32756  fmla0  32757  fmlasuc0  32759  satfdmfmla  32775  finxpsuclem  34833
 Copyright terms: Public domain W3C validator