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

Theorem elsuci 6432
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 6371 . . . 4 suc 𝐵 = (𝐵 ∪ {𝐵})
21eleq2i 2826 . . 3 (𝐴 ∈ suc 𝐵𝐴 ∈ (𝐵 ∪ {𝐵}))
3 elun 4149 . . 3 (𝐴 ∈ (𝐵 ∪ {𝐵}) ↔ (𝐴𝐵𝐴 ∈ {𝐵}))
42, 3bitri 275 . 2 (𝐴 ∈ suc 𝐵 ↔ (𝐴𝐵𝐴 ∈ {𝐵}))
5 elsni 4646 . . 3 (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)
65orim2i 910 . 2 ((𝐴𝐵𝐴 ∈ {𝐵}) → (𝐴𝐵𝐴 = 𝐵))
74, 6sylbi 216 1 (𝐴 ∈ suc 𝐵 → (𝐴𝐵𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 846   = wceq 1542  wcel 2107  cun 3947  {csn 4629  suc csuc 6367
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 3954  df-sn 4630  df-suc 6371
This theorem is referenced by:  suctr  6451  trsucss  6453  ordnbtwn  6458  suc11  6472  tfrlem11  8388  omordi  8566  nnmordi  8631  pssnn  9168  phplem3OLD  9219  pssnnOLD  9265  r1sdom  9769  cfsuc  10252  axdc3lem2  10446  axdc3lem4  10448  indpi  10902  bnj563  33754  bnj964  33954  ontgval  35316  onsucconni  35322  suctrALT  43587  suctrALT2VD  43597  suctrALT2  43598  suctrALTcf  43683  suctrALTcfVD  43684  suctrALT3  43685
  Copyright terms: Public domain W3C validator