| 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 4178 | . 2 ⊢ 𝐴 ⊆ (𝐴 ∪ {𝐴}) | |
| 2 | df-suc 6390 | . 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴}) | |
| 3 | 1, 2 | sseqtrri 4033 | 1 ⊢ 𝐴 ⊆ suc 𝐴 |
| Colors of variables: wff setvar class |
| Syntax hints: ∪ cun 3949 ⊆ wss 3951 {csn 4626 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-ss 3968 df-suc 6390 |
| This theorem is referenced by: trsuc 6471 sucexeloniOLD 7830 suceloniOLD 7832 limsssuc 7871 oaordi 8584 omeulem1 8620 oelim2 8633 nnaordi 8656 naddcllem 8714 phplem2 9245 php 9247 phplem4OLD 9257 phpOLD 9259 onomeneqOLD 9266 enp1i 9313 fiint 9366 fiintOLD 9367 cantnfval2 9709 cantnfle 9711 cantnfp1lem3 9720 cnfcomlem 9739 ttrclss 9760 ranksuc 9905 fseqenlem1 10064 pwsdompw 10243 fin1a2lem12 10451 canthp1lem2 10693 nosupbnd1 27759 nosupbnd2lem1 27760 noinfbnd1 27774 noinfbnd2lem1 27775 satfvsucsuc 35370 satffunlem2lem2 35411 satffunlem2 35413 limsucncmpi 36446 finxpreclem3 37394 insucid 43416 minregex 43547 clsk1independent 44059 grur1cld 44251 suctrALT 44846 suctrALT2VD 44856 suctrALT2 44857 suctrALTcf 44942 suctrALTcfVD 44943 suctrALT3 44944 |
| Copyright terms: Public domain | W3C validator |