![]() |
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 866 | . 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)) | |
2 | elsucg 6429 | . 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ suc 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))) | |
3 | 1, 2 | mpbird 257 | 1 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ suc 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 846 = wceq 1542 ∈ wcel 2107 suc csuc 6363 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-un 3952 df-sn 4628 df-suc 6367 |
This theorem is referenced by: suctr 6447 pssnn 9164 pssnnOLD 9261 ttrcltr 9707 ttrclss 9711 ttrclselem2 9717 pwsdompw 10195 fin1a2lem4 10394 grur1a 10810 bnj570 33854 satom 34285 satfv0 34287 satfvsuc 34290 satf00 34303 satf0suc 34305 sat1el2xp 34308 fmla 34310 fmla0 34311 fmlasuc0 34313 satfdmfmla 34329 finxpsuclem 36216 |
Copyright terms: Public domain | W3C validator |