Theorem elsuci 6257

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 6197	. . . 4 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵})
2	1	eleq2i 2822	. . 3 ⊢ (𝐴 ∈ suc 𝐵 ↔ 𝐴 ∈ (𝐵 ∪ {𝐵}))
3		elun 4049	. . 3 ⊢ (𝐴 ∈ (𝐵 ∪ {𝐵}) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ {𝐵}))
4	2, 3	bitri 278	. 2 ⊢ (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ {𝐵}))
5		elsni 4544	. . 3 ⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵)
6	5	orim2i 911	. 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ {𝐵}) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))
7	4, 6	sylbi 220	1 ⊢ (𝐴 ∈ suc 𝐵 → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1543   ∈ wcel 2112   ∪ cun 3851  {csn 4527  suc csuc 6193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-un 3858  df-sn 4528  df-suc 6197

This theorem is referenced by:  suctr  6274  trsucss  6276  ordnbtwn  6281  suc11  6294  tfrlem11  8102  omordi  8272  nnmordi  8337  phplem3  8805  pssnn  8824  pssnnOLD  8872  r1sdom  9355  cfsuc  9836  axdc3lem2  10030  axdc3lem4  10032  indpi  10486  bnj563  32389  bnj964  32590  ontgval  34306  onsucconni  34312  suctrALT  42060  suctrALT2VD  42070  suctrALT2  42071  suctrALTcf  42156  suctrALTcfVD  42157  suctrALT3  42158