Theorem elsuci 6443

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 6382	. . . 4 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵})
2	1	eleq2i 2818	. . 3 ⊢ (𝐴 ∈ suc 𝐵 ↔ 𝐴 ∈ (𝐵 ∪ {𝐵}))
3		elun 4148	. . 3 ⊢ (𝐴 ∈ (𝐵 ∪ {𝐵}) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ {𝐵}))
4	2, 3	bitri 274	. 2 ⊢ (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ {𝐵}))
5		elsni 4650	. . 3 ⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)
6	5	orim2i 908	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ {𝐵}) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))
7	4, 6	sylbi 216	1 ⊢ (𝐴 ∈ suc 𝐵 → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))

Syntax hints:   → wi 4   ∨ wo 845   = wceq 1534   ∈ wcel 2099   ∪ cun 3945  {csn 4633  suc csuc 6378

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-un 3952  df-sn 4634  df-suc 6382

This theorem is referenced by:  suctr  6462  trsucss  6464  ordnbtwn  6469  suc11  6483  tfrlem11  8418  omordi  8596  nnmordi  8661  pssnn  9206  phplem3OLD  9253  pssnnOLD  9299  r1sdom  9817  cfsuc  10300  axdc3lem2  10494  axdc3lem4  10496  indpi  10950  constrmon  33602  bnj563  34588  bnj964  34788  ontgval  36143  onsucconni  36149  suctrALT  44502  suctrALT2VD  44512  suctrALT2  44513  suctrALTcf  44598  suctrALTcfVD  44599  suctrALT3  44600