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

Theorem elsuci 6451
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 6390 . . . 4 suc 𝐵 = (𝐵 ∪ {𝐵})
21eleq2i 2833 . . 3 (𝐴 ∈ suc 𝐵𝐴 ∈ (𝐵 ∪ {𝐵}))
3 elun 4153 . . 3 (𝐴 ∈ (𝐵 ∪ {𝐵}) ↔ (𝐴𝐵𝐴 ∈ {𝐵}))
42, 3bitri 275 . 2 (𝐴 ∈ suc 𝐵 ↔ (𝐴𝐵𝐴 ∈ {𝐵}))
5 elsni 4643 . . 3 (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)
65orim2i 911 . 2 ((𝐴𝐵𝐴 ∈ {𝐵}) → (𝐴𝐵𝐴 = 𝐵))
74, 6sylbi 217 1 (𝐴 ∈ suc 𝐵 → (𝐴𝐵𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 848   = wceq 1540  wcel 2108  cun 3949  {csn 4626  suc csuc 6386
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-sn 4627  df-suc 6390
This theorem is referenced by:  suctr  6470  trsucss  6472  ordnbtwn  6477  suc11  6491  tfrlem11  8428  omordi  8604  nnmordi  8669  pssnn  9208  phplem3OLD  9256  r1sdom  9814  cfsuc  10297  axdc3lem2  10491  axdc3lem4  10493  indpi  10947  constrmon  33785  bnj563  34757  bnj964  34957  ontgval  36432  onsucconni  36438  suctrALT  44846  suctrALT2VD  44856  suctrALT2  44857  suctrALTcf  44942  suctrALTcfVD  44943  suctrALT3  44944
  Copyright terms: Public domain W3C validator