Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ssid | Unicode version |
Description: Any class is a subclass of itself. Exercise 10 of [TakeutiZaring] p. 18. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
Ref | Expression |
---|---|
ssid |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 | . 2 | |
2 | 1 | ssriv 3141 | 1 |
Colors of variables: wff set class |
Syntax hints: wcel 2135 wss 3111 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-11 1493 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-in 3117 df-ss 3124 |
This theorem is referenced by: ssidd 3158 eqimssi 3193 eqimss2i 3194 inv1 3440 difid 3472 undifabs 3480 pwidg 3567 elssuni 3811 unimax 3817 intmin 3838 rintm 3952 iunpw 4452 sucprcreg 4520 tfisi 4558 peano5 4569 xpss1 4708 xpss2 4709 residm 4910 resdm 4917 resmpt3 4927 ssrnres 5040 cocnvss 5123 dffn3 5342 fimacnv 5608 foima2 5714 tfrlem1 6267 rdgss 6342 fpmg 6631 findcard2d 6848 findcard2sd 6849 f1finf1o 6903 fidcenumlemr 6911 casef 7044 nnnninf 7081 1idprl 7522 1idpru 7523 ltexprlemm 7532 suplocexprlemmu 7650 elq 9551 expcl 10463 serclim0 11232 fsum2d 11362 fsumabs 11392 fsumiun 11404 fprod2d 11550 reef11 11626 ressid 12398 topopn 12553 fiinbas 12594 topbas 12614 topcld 12656 ntrtop 12675 opnneissb 12702 opnssneib 12703 opnneiid 12711 idcn 12759 cnconst2 12780 lmres 12795 retopbas 13070 cnopncntop 13084 abscncf 13119 recncf 13120 imcncf 13121 cjcncf 13122 mulc1cncf 13123 cncfcn1cntop 13128 cncfmpt2fcntop 13132 addccncf 13133 cdivcncfap 13134 negfcncf 13136 expcncf 13139 cnrehmeocntop 13140 cnlimcim 13187 cnlimc 13188 cnlimci 13189 dvcnp2cntop 13210 dvcn 13211 dvef 13235 efcn 13236 |
Copyright terms: Public domain | W3C validator |