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

Theorem elsuci 6100
 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 6040 . . . 4 suc 𝐵 = (𝐵 ∪ {𝐵})
21eleq2i 2859 . . 3 (𝐴 ∈ suc 𝐵𝐴 ∈ (𝐵 ∪ {𝐵}))
3 elun 4016 . . 3 (𝐴 ∈ (𝐵 ∪ {𝐵}) ↔ (𝐴𝐵𝐴 ∈ {𝐵}))
42, 3bitri 267 . 2 (𝐴 ∈ suc 𝐵 ↔ (𝐴𝐵𝐴 ∈ {𝐵}))
5 elsni 4461 . . 3 (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)
65orim2i 895 . 2 ((𝐴𝐵𝐴 ∈ {𝐵}) → (𝐴𝐵𝐴 = 𝐵))
74, 6sylbi 209 1 (𝐴 ∈ suc 𝐵 → (𝐴𝐵𝐴 = 𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ wo 834   = wceq 1508   ∈ wcel 2051   ∪ cun 3829  {csn 4444  suc csuc 6036 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2752 This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2761  df-cleq 2773  df-clel 2848  df-nfc 2920  df-v 3419  df-un 3836  df-sn 4445  df-suc 6040 This theorem is referenced by:  suctr  6117  trsucss  6119  ordnbtwn  6124  suc11  6137  tfrlem11  7834  omordi  7999  nnmordi  8064  phplem3  8500  pssnn  8537  r1sdom  9003  cfsuc  9483  axdc3lem2  9677  axdc3lem4  9679  indpi  10133  bnj563  31694  bnj964  31894  ontgval  33339  onsucconni  33345  suctrALT  40619  suctrALT2VD  40629  suctrALT2  40630  suctrALTcf  40715  suctrALTcfVD  40716  suctrALT3  40717
 Copyright terms: Public domain W3C validator