![]() |
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 4170 | . 2 ⊢ 𝐴 ⊆ (𝐴 ∪ {𝐴}) | |
2 | df-suc 6377 | . 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴}) | |
3 | 1, 2 | sseqtrri 4014 | 1 ⊢ 𝐴 ⊆ suc 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ∪ cun 3942 ⊆ wss 3944 {csn 4630 suc csuc 6373 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-v 3463 df-un 3949 df-ss 3961 df-suc 6377 |
This theorem is referenced by: trsuc 6458 sucexeloniOLD 7814 suceloniOLD 7816 limsssuc 7855 oaordi 8567 omeulem1 8603 oelim2 8616 nnaordi 8639 naddcllem 8697 phplem2 9233 php 9235 phplem4OLD 9245 phpOLD 9247 onomeneqOLD 9254 enp1i 9304 fiint 9350 cantnfval2 9694 cantnfle 9696 cantnfp1lem3 9705 cnfcomlem 9724 ttrclss 9745 ranksuc 9890 fseqenlem1 10049 pwsdompw 10229 fin1a2lem12 10436 canthp1lem2 10678 nosupbnd1 27693 nosupbnd2lem1 27694 noinfbnd1 27708 noinfbnd2lem1 27709 satfvsucsuc 35106 satffunlem2lem2 35147 satffunlem2 35149 limsucncmpi 36060 finxpreclem3 37003 insucid 42975 minregex 43106 clsk1independent 43618 grur1cld 43811 suctrALT 44407 suctrALT2VD 44417 suctrALT2 44418 suctrALTcf 44503 suctrALTcfVD 44504 suctrALT3 44505 |
Copyright terms: Public domain | W3C validator |