Theorem elsuci 6371

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

Step	Hyp	Ref	Expression
1		df-suc 6308	. . . 4 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵})
2	1	eleq2i 2821	. . 3 ⊢ (𝐴 ∈ suc 𝐵 ↔ 𝐴 ∈ (𝐵 ∪ {𝐵}))
3		elun 4101	. . 3 ⊢ (𝐴 ∈ (𝐵 ∪ {𝐵}) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ {𝐵}))
4	2, 3	bitri 275	. 2 ⊢ (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ {𝐵}))
5		elsni 4591	. . 3 ⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)
6	5	orim2i 910	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ {𝐵}) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))
7	4, 6	sylbi 217	1 ⊢ (𝐴 ∈ suc 𝐵 → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1541   ∈ wcel 2110   ∪ cun 3898  {csn 4574  suc csuc 6304

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3436  df-un 3905  df-sn 4575  df-suc 6308

This theorem is referenced by:  suctr  6390  trsucss  6392  ordnbtwn  6397  suc11  6411  tfrlem11  8302  omordi  8476  nnmordi  8541  pssnn  9073  r1sdom  9659  cfsuc  10140  axdc3lem2  10334  axdc3lem4  10336  indpi  10790  constrmon  33747  bnj563  34745  bnj964  34945  ontgval  36444  onsucconni  36450  suctrALT  44837  suctrALT2VD  44847  suctrALT2  44848  suctrALTcf  44933  suctrALTcfVD  44934  suctrALT3  44935