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

Theorem elsuci 6229
 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 6169 . . . 4 suc 𝐵 = (𝐵 ∪ {𝐵})
21eleq2i 2884 . . 3 (𝐴 ∈ suc 𝐵𝐴 ∈ (𝐵 ∪ {𝐵}))
3 elun 4079 . . 3 (𝐴 ∈ (𝐵 ∪ {𝐵}) ↔ (𝐴𝐵𝐴 ∈ {𝐵}))
42, 3bitri 278 . 2 (𝐴 ∈ suc 𝐵 ↔ (𝐴𝐵𝐴 ∈ {𝐵}))
5 elsni 4545 . . 3 (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)
65orim2i 908 . 2 ((𝐴𝐵𝐴 ∈ {𝐵}) → (𝐴𝐵𝐴 = 𝐵))
74, 6sylbi 220 1 (𝐴 ∈ suc 𝐵 → (𝐴𝐵𝐴 = 𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ wo 844   = wceq 1538   ∈ wcel 2112   ∪ cun 3882  {csn 4528  suc csuc 6165 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 2114  ax-9 2122  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-un 3889  df-sn 4529  df-suc 6169 This theorem is referenced by:  suctr  6246  trsucss  6248  ordnbtwn  6253  suc11  6266  tfrlem11  8011  omordi  8179  nnmordi  8244  phplem3  8686  pssnn  8724  r1sdom  9191  cfsuc  9672  axdc3lem2  9866  axdc3lem4  9868  indpi  10322  bnj563  32128  bnj964  32329  ontgval  33893  onsucconni  33899  suctrALT  41525  suctrALT2VD  41535  suctrALT2  41536  suctrALTcf  41621  suctrALTcfVD  41622  suctrALT3  41623
 Copyright terms: Public domain W3C validator