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 6280 | . 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))) | |
3 | 1, 2 | mpbird 260 | 1 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ suc 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 847 = wceq 1543 ∈ wcel 2110 suc csuc 6215 |
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 2016 ax-8 2112 ax-9 2120 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 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3410 df-un 3871 df-sn 4542 df-suc 6219 |
This theorem is referenced by: suctr 6296 pssnn 8846 pssnnOLD 8895 pwsdompw 9818 fin1a2lem4 10017 grur1a 10433 bnj570 32598 satom 33031 satfv0 33033 satfvsuc 33036 satf00 33049 satf0suc 33051 sat1el2xp 33054 fmla 33056 fmla0 33057 fmlasuc0 33059 satfdmfmla 33075 ttrcltr 33515 ttrclss 33519 finxpsuclem 35305 |
Copyright terms: Public domain | W3C validator |