![]() |
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 5946 | . 2 ⊢ (𝐴 ∈ V → 𝐴 ∈ suc 𝐴) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝐴 ∈ suc 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2144 Vcvv 3349 suc csuc 5868 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1990 ax-6 2056 ax-7 2092 ax-9 2153 ax-10 2173 ax-11 2189 ax-12 2202 ax-13 2407 ax-ext 2750 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 827 df-tru 1633 df-ex 1852 df-nf 1857 df-sb 2049 df-clab 2757 df-cleq 2763 df-clel 2766 df-nfc 2901 df-v 3351 df-un 3726 df-sn 4315 df-suc 5872 |
This theorem is referenced by: eqelsuc 5949 unon 7177 onuninsuci 7186 tfinds 7205 peano5 7235 tfrlem16 7641 oawordeulem 7787 oalimcl 7793 omlimcl 7811 oneo 7814 omeulem1 7815 oeworde 7826 nnawordex 7870 nnneo 7884 phplem4 8297 php 8299 fiint 8392 inf0 8681 oancom 8711 cantnfval2 8729 cantnflt 8732 cantnflem1 8749 cnfcom 8760 cnfcom2 8762 cnfcom3lem 8763 cnfcom3 8764 r1val1 8812 rankxplim3 8907 cardlim 8997 fseqenlem1 9046 cardaleph 9111 pwsdompw 9227 cfsmolem 9293 axdc3lem4 9476 ttukeylem5 9536 ttukeylem6 9537 ttukeylem7 9538 canthp1lem2 9676 pwxpndom2 9688 winainflem 9716 winalim2 9719 nqereu 9952 bnj216 31132 bnj98 31269 dfrdg2 32031 dford3lem2 38113 pw2f1ocnv 38123 aomclem1 38143 |
Copyright terms: Public domain | W3C validator |