![]() |
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 4330 | . . 3 ⊢ ¬ 𝑥 ∈ ∅ | |
2 | 1 | pm2.21i 119 | . 2 ⊢ (𝑥 ∈ ∅ → 𝑥 ∈ 𝐴) |
3 | 2 | ssriv 3980 | 1 ⊢ ∅ ⊆ 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2098 ⊆ wss 3944 ∅c0 4322 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-dif 3947 df-ss 3961 df-nul 4323 |
This theorem is referenced by: ss0b 4399 0pss 4446 npss0 4447 ssdifeq0 4488 pwpw0 4818 sssn 4831 sspr 4838 sstp 4839 uni0 4939 int0el 4983 0disj 5141 disjx0 5143 tr0 5279 al0ssb 5309 0elpw 5356 rel0 5801 0ima 6082 dmxpss 6177 dmsnopss 6220 dfpo2 6302 on0eqel 6495 iotassuni 6521 iotassuniOLD 6528 fun0 6619 f0 6778 fvmptss 7016 fvmptss2 7030 funressn 7168 riotassuni 7416 ordsuci 7812 frxp 8131 suppssdm 8182 suppun 8189 suppss 8199 suppssOLD 8200 suppssov1 8203 suppssov2 8204 suppss2 8206 suppssfv 8208 oaword1 8573 oaword2 8574 omwordri 8593 oewordri 8613 oeworde 8614 nnaword1 8650 naddword1 8712 mapssfset 8870 0domgOLD 9126 fodomr 9153 pwdom 9154 php 9235 phpOLD 9247 isinf 9285 isinfOLD 9286 finsschain 9385 fipwuni 9451 fipwss 9454 wdompwdom 9603 inf3lemd 9652 inf3lem1 9653 cantnfle 9696 ttrclselem1 9750 tc0 9772 r1val1 9811 alephgeom 10107 infmap2 10243 cfub 10274 cf0 10276 cflecard 10278 cfle 10279 fin23lem16 10360 itunitc1 10445 ttukeylem6 10539 ttukeylem7 10540 canthwe 10676 wun0 10743 tsk0 10788 gruina 10843 grur1a 10844 uzssz 12876 xrsup0 13337 fzoss1 13694 fsuppmapnn0fiubex 13993 swrd00 14630 swrdlend 14639 repswswrd 14770 xptrrel 14963 relexpdmd 15027 relexprnd 15031 relexpfldd 15033 rtrclreclem4 15044 sum0 15703 fsumss 15707 fsumcvg3 15711 prod0 15923 0bits 16417 sadid1 16446 sadid2 16447 smu01lem 16463 smu01 16464 smu02 16465 lcmf0 16608 vdwmc2 16951 vdwlem13 16965 ramz2 16996 strfvss 17159 ressbasssg 17220 ressbasssOLD 17223 ress0 17227 ismred2 17586 acsfn 17642 acsfn0 17643 0ssc 17826 fullfunc 17898 fthfunc 17899 mrelatglb0 18556 cntzssv 19291 symgsssg 19434 efgsfo 19706 dprdsn 20005 lsp0 20905 lss0v 20913 lspsnat 21045 lsppratlem3 21049 lbsexg 21064 evpmss 21535 ocv0 21626 ocvz 21627 css1 21639 resspsrbas 21936 mhp0cl 22093 psr1crng 22129 psr1assa 22130 psr1tos 22131 psr1bas2 22132 vr1cl2 22135 ply1lss 22139 ply1subrg 22140 psr1plusg 22163 psr1vsca 22164 psr1mulr 22165 psr1ring 22189 psr1lmod 22191 psr1sca 22192 0opn 22850 toponsspwpw 22868 basdif0 22900 baspartn 22901 0cld 22986 ntr0 23029 cmpfi 23356 refun0 23463 xkouni 23547 xkoccn 23567 alexsubALTlem2 23996 ptcmplem2 24001 tsmsfbas 24076 setsmstopn 24430 restmetu 24523 tngtopn 24611 iccntr 24781 xrge0gsumle 24793 xrge0tsms 24794 metdstri 24811 ovol0 25466 0mbl 25512 itg1le 25687 itgioo 25789 limcnlp 25851 dvbsss 25875 plyssc 26179 fsumharmonic 26989 nulsslt 27776 nulssgt 27777 bday0b 27809 madess 27849 oldssmade 27850 precsexlem8 28162 egrsubgr 29162 0grsubgr 29163 0uhgrsubgr 29164 chocnul 31210 span0 31424 chsup0 31430 ssnnssfz 32637 xrge0tsmsd 32861 unitprodclb 33201 ddemeas 33986 dya2iocuni 34034 oms0 34048 0elcarsg 34058 eulerpartlemt 34122 bnj1143 34552 mrsubrn 35254 msubrn 35270 mthmpps 35323 bj-nuliotaALT 36668 bj-restsn0 36695 bj-restsn10 36696 bj-imdirco 36800 pibt2 37027 mblfinlem2 37262 mblfinlem3 37263 ismblfin 37265 sstotbnd2 37378 isbnd3 37388 ssbnd 37392 heiborlem6 37420 lub0N 38791 glb0N 38795 0psubN 39352 padd01 39414 padd02 39415 pol0N 39512 pcl0N 39525 0psubclN 39546 mzpcompact2lem 42313 itgocn 42730 oaabsb 42865 oege1 42877 nnoeomeqom 42883 cantnfresb 42895 omabs2 42903 omcl2 42904 tfsconcatb0 42915 nadd2rabex 42957 fpwfvss 42984 nla0002 42996 nla0003 42997 nla0001 42998 fvnonrel 43169 clcnvlem 43195 cnvrcl0 43197 cnvtrcl0 43198 0he 43354 ntrclskb 43641 gru0eld 43808 mnu0eld 43844 mnuprdlem4 43854 mnuprd 43855 founiiun0 44702 uzfissfz 44846 limcdm0 45144 cncfiooicc 45420 itgvol0 45494 ibliooicc 45497 ovn0 46092 sprssspr 46958 isubgr0uhgr 47343 ssnn0ssfz 47599 ipolub0 48189 ipoglb0 48191 setrec2fun 48309 setrec2mpt 48314 |
Copyright terms: Public domain | W3C validator |