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

Step	Hyp	Ref	Expression
1		df-suc 6040	. . . 4 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵})
2	1	eleq2i 2859	. . 3 ⊢ (𝐴 ∈ suc 𝐵 ↔ 𝐴 ∈ (𝐵 ∪ {𝐵}))
3		elun 4016	. . 3 ⊢ (𝐴 ∈ (𝐵 ∪ {𝐵}) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ {𝐵}))
4	2, 3	bitri 267	. 2 ⊢ (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ {𝐵}))
5		elsni 4461	. . 3 ⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)
6	5	orim2i 895	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ {𝐵}) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))
7	4, 6	sylbi 209	1 ⊢ (𝐴 ∈ suc 𝐵 → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))

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