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

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

Proof of Theorem elelsuc
StepHypRef Expression
1 orc 866 . 2 (𝐴𝐵 → (𝐴𝐵𝐴 = 𝐵))
2 elsucg 6429 . 2 (𝐴𝐵 → (𝐴 ∈ suc 𝐵 ↔ (𝐴𝐵𝐴 = 𝐵)))
31, 2mpbird 257 1 (𝐴𝐵𝐴 ∈ suc 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 846   = wceq 1542  wcel 2107  suc csuc 6363
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3952  df-sn 4628  df-suc 6367
This theorem is referenced by:  suctr  6447  pssnn  9164  pssnnOLD  9261  ttrcltr  9707  ttrclss  9711  ttrclselem2  9717  pwsdompw  10195  fin1a2lem4  10394  grur1a  10810  bnj570  33854  satom  34285  satfv0  34287  satfvsuc  34290  satf00  34303  satf0suc  34305  sat1el2xp  34308  fmla  34310  fmla0  34311  fmlasuc0  34313  satfdmfmla  34329  finxpsuclem  36216
  Copyright terms: Public domain W3C validator