![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elelsuc | Structured version Visualization version GIF version |
Description: Membership in a successor. (Contributed by NM, 20-Jun-1998.) |
Ref | Expression |
---|---|
elelsuc | ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ suc 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orc 867 | . 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)) | |
2 | elsucg 6454 | . 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))) | |
3 | 1, 2 | mpbird 257 | 1 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ suc 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 847 = wceq 1537 ∈ wcel 2106 suc csuc 6388 |
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 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1540 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-v 3480 df-un 3968 df-sn 4632 df-suc 6392 |
This theorem is referenced by: suctr 6472 pssnn 9207 ttrcltr 9754 ttrclss 9758 ttrclselem2 9764 pwsdompw 10241 fin1a2lem4 10441 grur1a 10857 bnj570 34898 satom 35341 satfv0 35343 satfvsuc 35346 satf00 35359 satf0suc 35361 sat1el2xp 35364 fmla 35366 fmla0 35367 fmlasuc0 35369 satfdmfmla 35385 finxpsuclem 37380 |
Copyright terms: Public domain | W3C validator |