|   | 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 6451 | . 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))) | |
| 3 | 1, 2 | mpbird 257 | 1 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ suc 𝐵) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∨ wo 847 = wceq 1539 ∈ wcel 2107 suc csuc 6385 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-v 3481 df-un 3955 df-sn 4626 df-suc 6389 | 
| This theorem is referenced by: suctr 6469 pssnn 9209 ttrcltr 9757 ttrclss 9761 ttrclselem2 9767 pwsdompw 10244 fin1a2lem4 10444 grur1a 10860 bnj570 34920 satom 35362 satfv0 35364 satfvsuc 35367 satf00 35380 satf0suc 35382 sat1el2xp 35385 fmla 35387 fmla0 35388 fmlasuc0 35390 satfdmfmla 35406 finxpsuclem 37399 | 
| Copyright terms: Public domain | W3C validator |