Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 0ss | Structured version Visualization version Unicode version |
Description: The null set is a subset of any class. Part of Exercise 1 of [TakeutiZaring] p. 22. (Contributed by NM, 21-Jun-1993.) |
Ref | Expression |
---|---|
0ss |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | noel 3919 | . . 3 | |
2 | 1 | pm2.21i 116 | . 2 |
3 | 2 | ssriv 3607 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wcel 1990 wss 3574 c0 3915 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 df-dif 3577 df-in 3581 df-ss 3588 df-nul 3916 |
This theorem is referenced by: ss0b 3973 0pss 4013 npss0 4014 npss0OLD 4015 ssdifeq0 4051 pwpw0 4344 sssn 4358 sspr 4366 sstp 4367 pwsnALT 4429 uni0 4465 int0el 4508 0disj 4645 disjx0 4647 tr0 4764 0elpw 4834 rel0 5243 0ima 5482 dmxpss 5565 dmsnopss 5607 on0eqel 5845 iotassuni 5867 fun0 5954 fresaunres2 6076 f0 6086 fvmptss 6292 fvmptss2 6304 funressn 6426 riotassuni 6648 frxp 7287 suppssdm 7308 suppun 7315 suppss 7325 suppssov1 7327 suppss2 7329 suppssfv 7331 oaword1 7632 oaword2 7633 omwordri 7652 oewordri 7672 oeworde 7673 nnaword1 7709 0domg 8087 fodomr 8111 pwdom 8112 php 8144 isinf 8173 finsschain 8273 fipwuni 8332 fipwss 8335 wdompwdom 8483 inf3lemd 8524 inf3lem1 8525 cantnfle 8568 tc0 8623 r1val1 8649 alephgeom 8905 infmap2 9040 cfub 9071 cf0 9073 cflecard 9075 cfle 9076 fin23lem16 9157 itunitc1 9242 ttukeylem6 9336 ttukeylem7 9337 canthwe 9473 wun0 9540 tsk0 9585 gruina 9640 grur1a 9641 uzssz 11707 xrsup0 12153 fzoss1 12495 fsuppmapnn0fiubex 12792 swrd00 13418 swrdlend 13431 swrd0 13434 repswswrd 13531 xptrrel 13719 sum0 14452 fsumss 14456 fsumcvg3 14460 prod0 14673 0bits 15161 sadid1 15190 sadid2 15191 smu01lem 15207 smu01 15208 smu02 15209 lcmf0 15347 vdwmc2 15683 vdwlem13 15697 ramz2 15728 strfvss 15880 ressbasss 15932 ress0 15934 strlemor0OLD 15968 ismred2 16263 acsfn 16320 acsfn0 16321 0ssc 16497 fullfunc 16566 fthfunc 16567 mrelatglb0 17185 cntzssv 17761 symgsssg 17887 efgsfo 18152 dprdsn 18435 lsp0 19009 lss0v 19016 lspsnat 19145 lsppratlem3 19149 lbsexg 19164 resspsrbas 19415 psr1crng 19557 psr1assa 19558 psr1tos 19559 psr1bas2 19560 vr1cl2 19563 ply1lss 19566 ply1subrg 19567 psr1plusg 19592 psr1vsca 19593 psr1mulr 19594 psr1ring 19617 psr1lmod 19619 psr1sca 19620 evpmss 19932 ocv0 20021 ocvz 20022 css1 20034 0opn 20709 toponsspwpw 20726 basdif0 20757 baspartn 20758 0cld 20842 cls0 20884 ntr0 20885 cmpfi 21211 refun0 21318 xkouni 21402 xkoccn 21422 alexsubALTlem2 21852 ptcmplem2 21857 tsmsfbas 21931 setsmstopn 22283 restmetu 22375 tngtopn 22454 iccntr 22624 xrge0gsumle 22636 xrge0tsms 22637 metdstri 22654 ovol0 23261 0mbl 23307 itg1le 23480 itgioo 23582 limcnlp 23642 dvbsss 23666 plyssc 23956 fsumharmonic 24738 egrsubgr 26169 0grsubgr 26170 0uhgrsubgr 26171 chocnul 28187 span0 28401 chsup0 28407 ssnnssfz 29549 xrge0tsmsd 29785 ddemeas 30299 dya2iocuni 30345 oms0 30359 0elcarsg 30369 eulerpartlemt 30433 bnj1143 30861 mrsubrn 31410 msubrn 31426 mthmpps 31479 dfpo2 31645 trpredlem1 31727 nulsslt 31908 nulssgt 31909 bj-nuliotaALT 33020 bj-restsn0 33038 bj-restsn10 33039 bj-ismooredr2 33065 mblfinlem2 33447 mblfinlem3 33448 ismblfin 33450 sstotbnd2 33573 isbnd3 33583 ssbnd 33587 heiborlem6 33615 lub0N 34476 glb0N 34480 0psubN 35035 padd01 35097 padd02 35098 pol0N 35195 pcl0N 35208 0psubclN 35229 mzpcompact2lem 37314 itgocn 37734 fvnonrel 37903 clcnvlem 37930 cnvrcl0 37932 cnvtrcl0 37933 0he 38076 ntrclskb 38367 founiiun0 39377 uzfissfz 39542 limcdm0 39850 cncfiooicc 40107 itgvol0 40184 ibliooicc 40187 ovn0 40780 sprssspr 41731 ssnn0ssfz 42127 setrec2fun 42439 |
Copyright terms: Public domain | W3C validator |