Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > sucid | Structured version Visualization version GIF version |
Description: A set belongs to its successor. (Contributed by NM, 22-Jun-1994.) (Proof shortened by Alan Sare, 18-Feb-2012.) (Proof shortened by Scott Fenton, 20-Feb-2012.) |
Ref | Expression |
---|---|
sucid.1 | ⊢ 𝐴 ∈ V |
Ref | Expression |
---|---|
sucid | ⊢ 𝐴 ∈ suc 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sucid.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | sucidg 6261 | . 2 ⊢ (𝐴 ∈ V → 𝐴 ∈ suc 𝐴) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝐴 ∈ suc 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2114 Vcvv 3400 suc csuc 6185 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2711 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-tru 1545 df-ex 1787 df-sb 2075 df-clab 2718 df-cleq 2731 df-clel 2812 df-v 3402 df-un 3858 df-sn 4527 df-suc 6189 |
This theorem is referenced by: eqelsuc 6264 unon 7578 onuninsuci 7587 tfinds 7606 peano5 7637 peano5OLD 7638 tfrlem16 8071 oawordeulem 8224 oalimcl 8230 omlimcl 8248 oneo 8251 omeulem1 8252 oeworde 8263 nnawordex 8307 nnneo 8322 phplem4 8762 php 8764 fiint 8882 inf0 9170 oancom 9200 cantnfval2 9218 cantnflt 9221 cantnflem1 9238 cnfcom 9249 cnfcom2 9251 cnfcom3lem 9252 cnfcom3 9253 r1val1 9301 rankxplim3 9396 cardlim 9487 fseqenlem1 9537 cardaleph 9602 pwsdompw 9717 cfsmolem 9783 axdc3lem4 9966 ttukeylem5 10026 ttukeylem6 10027 ttukeylem7 10028 canthp1lem2 10166 pwxpndom2 10178 winainflem 10206 winalim2 10209 nqereu 10442 bnj216 32294 bnj98 32431 satom 32902 fmla 32927 ex-sategoelel12 32973 dfrdg2 33358 naddcllem 33487 nogt01o 33555 dford3lem2 40462 pw2f1ocnv 40472 aomclem1 40492 |
Copyright terms: Public domain | W3C validator |