Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 0ss | Structured version Visualization version GIF 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 4298 | . . 3 ⊢ ¬ 𝑥 ∈ ∅ | |
2 | 1 | pm2.21i 119 | . 2 ⊢ (𝑥 ∈ ∅ → 𝑥 ∈ 𝐴) |
3 | 2 | ssriv 3973 | 1 ⊢ ∅ ⊆ 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2114 ⊆ wss 3938 ∅c0 4293 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2802 df-cleq 2816 df-clel 2895 df-dif 3941 df-in 3945 df-ss 3954 df-nul 4294 |
This theorem is referenced by: ss0b 4353 0pss 4398 npss0 4399 ssdifeq0 4434 pwpw0 4748 sssn 4761 sspr 4768 sstp 4769 pwsnOLD 4833 uni0 4868 int0el 4909 0disj 5060 disjx0 5062 tr0 5185 al0ssb 5214 0elpw 5258 rel0 5674 0ima 5948 dmxpss 6030 dmsnopss 6073 on0eqel 6310 iotassuni 6336 fun0 6421 f0 6562 fvmptss 6782 fvmptss2 6795 funressn 6923 riotassuni 7156 frxp 7822 suppssdm 7845 suppun 7852 suppss 7862 suppssov1 7864 suppss2 7866 suppssfv 7868 oaword1 8180 oaword2 8181 omwordri 8200 oewordri 8220 oeworde 8221 nnaword1 8257 0domg 8646 fodomr 8670 pwdom 8671 php 8703 isinf 8733 finsschain 8833 fipwuni 8892 fipwss 8895 wdompwdom 9044 inf3lemd 9092 inf3lem1 9093 cantnfle 9136 tc0 9191 r1val1 9217 alephgeom 9510 infmap2 9642 cfub 9673 cf0 9675 cflecard 9677 cfle 9678 fin23lem16 9759 itunitc1 9844 ttukeylem6 9938 ttukeylem7 9939 canthwe 10075 wun0 10142 tsk0 10187 gruina 10242 grur1a 10243 uzssz 12267 xrsup0 12719 fzoss1 13067 fsuppmapnn0fiubex 13363 swrd00 14008 swrdlend 14017 repswswrd 14148 xptrrel 14342 sum0 15080 fsumss 15084 fsumcvg3 15088 prod0 15299 0bits 15790 sadid1 15819 sadid2 15820 smu01lem 15836 smu01 15837 smu02 15838 lcmf0 15980 vdwmc2 16317 vdwlem13 16331 ramz2 16362 strfvss 16508 ressbasss 16558 ress0 16560 ismred2 16876 acsfn 16932 acsfn0 16933 0ssc 17109 fullfunc 17178 fthfunc 17179 mrelatglb0 17797 cntzssv 18460 symgsssg 18597 efgsfo 18867 dprdsn 19160 lsp0 19783 lss0v 19790 lspsnat 19919 lsppratlem3 19923 lbsexg 19938 resspsrbas 20197 mhp0cl 20339 psr1crng 20357 psr1assa 20358 psr1tos 20359 psr1bas2 20360 vr1cl2 20363 ply1lss 20366 ply1subrg 20367 psr1plusg 20392 psr1vsca 20393 psr1mulr 20394 psr1ring 20417 psr1lmod 20419 psr1sca 20420 evpmss 20732 ocv0 20823 ocvz 20824 css1 20836 0opn 21514 toponsspwpw 21532 basdif0 21563 baspartn 21564 0cld 21648 ntr0 21691 cmpfi 22018 refun0 22125 xkouni 22209 xkoccn 22229 alexsubALTlem2 22658 ptcmplem2 22663 tsmsfbas 22738 setsmstopn 23090 restmetu 23182 tngtopn 23261 iccntr 23431 xrge0gsumle 23443 xrge0tsms 23444 metdstri 23461 ovol0 24096 0mbl 24142 itg1le 24316 itgioo 24418 limcnlp 24478 dvbsss 24502 plyssc 24792 fsumharmonic 25591 egrsubgr 27061 0grsubgr 27062 0uhgrsubgr 27063 chocnul 29107 span0 29321 chsup0 29327 ssnnssfz 30512 xrge0tsmsd 30694 ddemeas 31497 dya2iocuni 31543 oms0 31557 0elcarsg 31567 eulerpartlemt 31631 bnj1143 32064 mrsubrn 32762 msubrn 32778 mthmpps 32831 dfpo2 32993 trpredlem1 33068 nulsslt 33264 nulssgt 33265 bj-nuliotaALT 34353 bj-restsn0 34378 bj-restsn10 34379 pibt2 34700 mblfinlem2 34932 mblfinlem3 34933 ismblfin 34935 sstotbnd2 35054 isbnd3 35064 ssbnd 35068 heiborlem6 35096 lub0N 36327 glb0N 36331 0psubN 36887 padd01 36949 padd02 36950 pol0N 37047 pcl0N 37060 0psubclN 37081 mzpcompact2lem 39355 itgocn 39771 fvnonrel 39964 clcnvlem 39990 cnvrcl0 39992 cnvtrcl0 39993 0he 40135 ntrclskb 40426 gru0eld 40572 mnu0eld 40608 mnuprdlem4 40618 mnuprd 40619 founiiun0 41458 uzfissfz 41601 limcdm0 41906 cncfiooicc 42184 itgvol0 42260 ibliooicc 42263 ovn0 42855 sprssspr 43650 ssnn0ssfz 44404 setrec2fun 44802 |
Copyright terms: Public domain | W3C validator |