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

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

Proof of Theorem elsuci
StepHypRef Expression
1 df-suc 6382 . . . 4 suc 𝐵 = (𝐵 ∪ {𝐵})
21eleq2i 2818 . . 3 (𝐴 ∈ suc 𝐵𝐴 ∈ (𝐵 ∪ {𝐵}))
3 elun 4148 . . 3 (𝐴 ∈ (𝐵 ∪ {𝐵}) ↔ (𝐴𝐵𝐴 ∈ {𝐵}))
42, 3bitri 274 . 2 (𝐴 ∈ suc 𝐵 ↔ (𝐴𝐵𝐴 ∈ {𝐵}))
5 elsni 4650 . . 3 (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)
65orim2i 908 . 2 ((𝐴𝐵𝐴 ∈ {𝐵}) → (𝐴𝐵𝐴 = 𝐵))
74, 6sylbi 216 1 (𝐴 ∈ suc 𝐵 → (𝐴𝐵𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 845   = wceq 1534  wcel 2099  cun 3945  {csn 4633  suc csuc 6378
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-un 3952  df-sn 4634  df-suc 6382
This theorem is referenced by:  suctr  6462  trsucss  6464  ordnbtwn  6469  suc11  6483  tfrlem11  8418  omordi  8596  nnmordi  8661  pssnn  9206  phplem3OLD  9253  pssnnOLD  9299  r1sdom  9817  cfsuc  10300  axdc3lem2  10494  axdc3lem4  10496  indpi  10950  constrmon  33602  bnj563  34588  bnj964  34788  ontgval  36143  onsucconni  36149  suctrALT  44502  suctrALT2VD  44512  suctrALT2  44513  suctrALTcf  44598  suctrALTcfVD  44599  suctrALT3  44600
  Copyright terms: Public domain W3C validator