![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sssucid | Structured version Visualization version Unicode 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 |
![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssun1 3599 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | df-suc 5432 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sseqtr4i 3467 |
1
![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-v 3049 df-un 3411 df-in 3413 df-ss 3420 df-suc 5432 |
This theorem is referenced by: trsuc 5510 suceloni 6645 limsssuc 6682 oaordi 7252 omeulem1 7288 oelim2 7301 nnaordi 7324 phplem4 7759 php 7761 onomeneq 7767 fiint 7853 cantnfval2 8179 cantnfle 8181 cantnfp1lem3 8190 cnfcomlem 8209 ranksuc 8341 fseqenlem1 8460 pwsdompw 8639 fin1a2lem12 8846 canthp1lem2 9083 nofulllem5 30607 limsucncmpi 31117 finxpreclem3 31797 suctrALT 37232 suctrALT2VD 37242 suctrALT2 37243 suctrALTcf 37329 suctrALTcfVD 37330 suctrALT3 37331 |
Copyright terms: Public domain | W3C validator |