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

Theorem elsuci 5779
Description: Membership in a successor. This one-way implication does not require that either 𝐴 or 𝐵 be sets. (Contributed by NM, 6-Jun-1994.)
Assertion
Ref Expression
elsuci (𝐴 ∈ suc 𝐵 → (𝐴𝐵𝐴 = 𝐵))

Proof of Theorem elsuci
StepHypRef Expression
1 df-suc 5717 . . . 4 suc 𝐵 = (𝐵 ∪ {𝐵})
21eleq2i 2691 . . 3 (𝐴 ∈ suc 𝐵𝐴 ∈ (𝐵 ∪ {𝐵}))
3 elun 3745 . . 3 (𝐴 ∈ (𝐵 ∪ {𝐵}) ↔ (𝐴𝐵𝐴 ∈ {𝐵}))
42, 3bitri 264 . 2 (𝐴 ∈ suc 𝐵 ↔ (𝐴𝐵𝐴 ∈ {𝐵}))
5 elsni 4185 . . 3 (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)
65orim2i 540 . 2 ((𝐴𝐵𝐴 ∈ {𝐵}) → (𝐴𝐵𝐴 = 𝐵))
74, 6sylbi 207 1 (𝐴 ∈ suc 𝐵 → (𝐴𝐵𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 383   = wceq 1481  wcel 1988  cun 3565  {csn 4168  suc csuc 5713
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-un 3572  df-sn 4169  df-suc 5717
This theorem is referenced by:  suctr  5796  trsucss  5799  ordnbtwn  5804  ordnbtwnOLD  5805  suc11  5819  tfrlem11  7469  omordi  7631  nnmordi  7696  phplem3  8126  pssnn  8163  r1sdom  8622  cfsuc  9064  axdc3lem2  9258  axdc3lem4  9260  indpi  9714  bnj563  30787  bnj964  30987  ontgval  32405  onsucconni  32411  suctrALT  38881  suctrALT2VD  38891  suctrALT2  38892  suctrALTcf  38978  suctrALTcfVD  38979  suctrALT3  38980
  Copyright terms: Public domain W3C validator