![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sucex | Structured version Visualization version GIF version |
Description: The successor of a set is a set. (Contributed by NM, 30-Aug-1993.) |
Ref | Expression |
---|---|
sucex.1 | ⊢ 𝐴 ∈ V |
Ref | Expression |
---|---|
sucex | ⊢ suc 𝐴 ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sucex.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | sucexg 7825 | . 2 ⊢ (𝐴 ∈ V → suc 𝐴 ∈ V) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ suc 𝐴 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 Vcvv 3478 suc csuc 6388 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 ax-sep 5302 ax-nul 5312 ax-pr 5438 ax-un 7754 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-rab 3434 df-v 3480 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-nul 4340 df-sn 4632 df-pr 4634 df-uni 4913 df-suc 6392 |
This theorem is referenced by: orduninsuc 7864 tfindsg 7882 tfinds2 7885 finds 7919 findsg 7920 finds2 7921 seqomlem1 8489 oasuc 8561 onasuc 8565 naddcllem 8713 infensuc 9194 phplem4OLD 9255 phpOLD 9257 inf0 9659 inf3lem1 9666 dfom3 9685 cantnflt 9710 cantnflem1 9727 cnfcom 9738 brttrcl2 9752 ssttrcl 9753 ttrcltr 9754 ttrclss 9758 ttrclselem2 9764 infxpenlem 10051 pwsdompw 10241 cfslb2n 10306 cfsmolem 10308 fin1a2lem12 10449 axdc4lem 10493 alephreg 10620 bnj986 34948 bnj1018g 34956 bnj1018 34957 satf 35338 dfon2lem7 35771 rdgssun 37361 dford3lem2 43016 |
Copyright terms: Public domain | W3C validator |