Theorem elsuci 6430

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 6366	. . . 4 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵})
2	1	eleq2i 2854	. . 3 ⊢ (𝐴 ∈ suc 𝐵 ↔ 𝐴 ∈ (𝐵 ∪ {𝐵}))
3		elun 4106	. . 3 ⊢ (𝐴 ∈ (𝐵 ∪ {𝐵}) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ {𝐵}))
4	2, 3	bitri 278	. 2 ⊢ (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ {𝐵}))
5		elsni 4605	. . 3 ⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)
6	5	orim2i 923	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ {𝐵}) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))
7	4, 6	sylbi 220	1 ⊢ (𝐴 ∈ suc 𝐵 → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))

This proof depends on syntax axioms:   → wi 4   ∨ wo 860   = wceq 1569   ∈ wcel 2142   ∪ cun 3902  {csn 4588  suc csuc 6362

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-un 3909  df-sn 4589  df-suc 6366

This theorem is used by:  suctr  6449  trsucss  6451  ordnbtwn  6456  suc11  6470  tfrlem11  8373  omordi  8549  nnmordi  8615  pssnn  9151  r1sdom  9744  cfsuc  10247  axdc3lem2  10441  axdc3lem4  10443  indpi  10898  constrmon  34143  bnj563  35141  bnj964  35340  ontgval  36970  onsucconni  36976  suctrALT  45562  suctrALT2VD  45572  suctrALT2  45573  suctrALTcf  45658  suctrALTcfVD  45659  suctrALT3  45660