| 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 6465 | . 2 ⊢ (𝐴 ∈ V → 𝐴 ∈ suc 𝐴) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝐴 ∈ suc 𝐴 |
| Colors of variables: wff setvar class |
| Syntax hints: ∈ wcel 2108 Vcvv 3480 suc csuc 6386 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-un 3956 df-sn 4627 df-suc 6390 |
| This theorem is referenced by: eqelsuc 6468 unon 7851 onuninsuci 7861 tfinds 7881 peano5 7915 tfrlem16 8433 oawordeulem 8592 oalimcl 8598 omlimcl 8616 oneo 8619 omeulem1 8620 oeworde 8631 nnawordex 8675 nnneo 8693 naddcllem 8714 phplem2 9245 php 9247 phplem4OLD 9257 phpOLD 9259 fiint 9366 fiintOLD 9367 inf0 9661 oancom 9691 cantnfval2 9709 cantnflt 9712 cantnflem1 9729 cnfcom 9740 cnfcom2 9742 cnfcom3lem 9743 cnfcom3 9744 ssttrcl 9755 ttrcltr 9756 ttrclss 9760 rnttrcl 9762 ttrclselem2 9766 r1val1 9826 rankxplim3 9921 cardlim 10012 fseqenlem1 10064 cardaleph 10129 pwsdompw 10243 cfsmolem 10310 axdc3lem4 10493 ttukeylem5 10553 ttukeylem6 10554 ttukeylem7 10555 canthp1lem2 10693 pwxpndom2 10705 winainflem 10733 winalim2 10736 nqereu 10969 nogt01o 27741 n0sbday 28354 pw2bday 28418 bnj216 34746 bnj98 34881 satom 35361 fmla 35386 ex-sategoelel12 35432 dfrdg2 35796 dford3lem2 43039 pw2f1ocnv 43049 aomclem1 43066 nnoeomeqom 43325 naddgeoa 43407 naddwordnexlem4 43414 |
| Copyright terms: Public domain | W3C validator |