![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sssucid | Structured version Visualization version GIF version |
Description: A class is included in its own successor. Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized to arbitrary classes). (Contributed by NM, 31-May-1994.) |
Ref | Expression |
---|---|
sssucid | ⊢ 𝐴 ⊆ suc 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssun1 4075 | . 2 ⊢ 𝐴 ⊆ (𝐴 ∪ {𝐴}) | |
2 | df-suc 6079 | . 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴}) | |
3 | 1, 2 | sseqtr4i 3931 | 1 ⊢ 𝐴 ⊆ suc 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ∪ cun 3863 ⊆ wss 3865 {csn 4478 suc csuc 6075 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-ext 2771 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-v 3442 df-un 3870 df-in 3872 df-ss 3880 df-suc 6079 |
This theorem is referenced by: trsuc 6157 suceloni 7391 limsssuc 7428 oaordi 8029 omeulem1 8065 oelim2 8078 nnaordi 8101 phplem4 8553 php 8555 onomeneq 8561 fiint 8648 cantnfval2 8985 cantnfle 8987 cantnfp1lem3 8996 cnfcomlem 9015 ranksuc 9147 fseqenlem1 9303 pwsdompw 9479 fin1a2lem12 9686 canthp1lem2 9928 satfvsucsuc 32222 satffunlem2lem2 32263 satffunlem2 32265 nosupbday 32816 nosupbnd1 32825 nosupbnd2lem1 32826 limsucncmpi 33404 finxpreclem3 34226 clsk1independent 39902 grur1cld 40086 suctrALT 40720 suctrALT2VD 40730 suctrALT2 40731 suctrALTcf 40816 suctrALTcfVD 40817 suctrALT3 40818 |
Copyright terms: Public domain | W3C validator |