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 6191 | . . . 4 ⊢ suc 𝐵 = (𝐵 ∪ {𝐵}) | |
2 | 1 | eleq2i 2904 | . . 3 ⊢ (𝐴 ∈ suc 𝐵 ↔ 𝐴 ∈ (𝐵 ∪ {𝐵})) |
3 | elun 4124 | . . 3 ⊢ (𝐴 ∈ (𝐵 ∪ {𝐵}) ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ {𝐵})) | |
4 | 2, 3 | bitri 277 | . 2 ⊢ (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 ∈ {𝐵})) |
5 | elsni 4577 | . . 3 ⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵) | |
6 | 5 | orim2i 907 | . 2 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 ∈ {𝐵}) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)) |
7 | 4, 6 | sylbi 219 | 1 ⊢ (𝐴 ∈ suc 𝐵 → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 843 = wceq 1533 ∈ wcel 2110 ∪ cun 3933 {csn 4560 suc csuc 6187 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-v 3496 df-un 3940 df-sn 4561 df-suc 6191 |
This theorem is referenced by: suctr 6268 trsucss 6270 ordnbtwn 6275 suc11 6288 tfrlem11 8018 omordi 8186 nnmordi 8251 phplem3 8692 pssnn 8730 r1sdom 9197 cfsuc 9673 axdc3lem2 9867 axdc3lem4 9869 indpi 10323 bnj563 32009 bnj964 32210 ontgval 33774 onsucconni 33780 suctrALT 41153 suctrALT2VD 41163 suctrALT2 41164 suctrALTcf 41249 suctrALTcfVD 41250 suctrALT3 41251 |
Copyright terms: Public domain | W3C validator |