![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elsuci | Structured version Visualization version GIF version |
Description: Membership in a successor. This one-way implication does not require that either 𝐴 or 𝐵 be sets. (Contributed by NM, 6-Jun-1994.) |
Ref | Expression |
---|---|
elsuci | ⊢ (𝐴 ∈ suc 𝐵 → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)) |
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 𝐵 → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)) |
Colors of variables: wff setvar class |
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 |
Copyright terms: Public domain | W3C validator |