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 6348 | . 2 ⊢ (𝐴 ∈ V → 𝐴 ∈ suc 𝐴) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝐴 ∈ suc 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2107 Vcvv 3433 suc csuc 6272 |
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 2710 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-tru 1542 df-ex 1783 df-sb 2069 df-clab 2717 df-cleq 2731 df-clel 2817 df-v 3435 df-un 3893 df-sn 4563 df-suc 6276 |
This theorem is referenced by: eqelsuc 6351 unon 7687 onuninsuci 7696 tfinds 7715 peano5 7749 peano5OLD 7750 tfrlem16 8233 oawordeulem 8394 oalimcl 8400 omlimcl 8418 oneo 8421 omeulem1 8422 oeworde 8433 nnawordex 8477 nnneo 8494 phplem2 9000 php 9002 phplem4OLD 9012 phpOLD 9014 fiint 9100 inf0 9388 oancom 9418 cantnfval2 9436 cantnflt 9439 cantnflem1 9456 cnfcom 9467 cnfcom2 9469 cnfcom3lem 9470 cnfcom3 9471 ssttrcl 9482 ttrcltr 9483 ttrclss 9487 rnttrcl 9489 ttrclselem2 9493 r1val1 9553 rankxplim3 9648 cardlim 9739 fseqenlem1 9789 cardaleph 9854 pwsdompw 9969 cfsmolem 10035 axdc3lem4 10218 ttukeylem5 10278 ttukeylem6 10279 ttukeylem7 10280 canthp1lem2 10418 pwxpndom2 10430 winainflem 10458 winalim2 10461 nqereu 10694 bnj216 32720 bnj98 32856 satom 33327 fmla 33352 ex-sategoelel12 33398 dfrdg2 33780 naddcllem 33840 nogt01o 33908 dford3lem2 40856 pw2f1ocnv 40866 aomclem1 40886 |
Copyright terms: Public domain | W3C validator |