![]() |
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 4148 | . . 3 ⊢ ¬ 𝑥 ∈ ∅ | |
2 | 1 | pm2.21i 117 | . 2 ⊢ (𝑥 ∈ ∅ → 𝑥 ∈ 𝐴) |
3 | 2 | ssriv 3831 | 1 ⊢ ∅ ⊆ 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2164 ⊆ wss 3798 ∅c0 4144 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-v 3416 df-dif 3801 df-in 3805 df-ss 3812 df-nul 4145 |
This theorem is referenced by: ss0b 4198 0pss 4238 npss0 4239 ssdifeq0 4274 pwpw0 4562 sssn 4575 sspr 4582 sstp 4583 pwsnALT 4651 uni0 4687 int0el 4728 0disj 4866 disjx0 4868 tr0 4986 al0ssb 5015 0elpw 5056 rel0 5457 0ima 5723 dmxpss 5806 dmsnopss 5848 on0eqel 6080 iotassuni 6102 fun0 6187 fresaunres2 6313 f0 6323 fvmptss 6539 fvmptss2 6552 funressn 6677 riotassuni 6903 frxp 7551 suppssdm 7572 suppun 7579 suppss 7590 suppssov1 7592 suppss2 7594 suppssfv 7596 oaword1 7899 oaword2 7900 omwordri 7919 oewordri 7939 oeworde 7940 nnaword1 7976 0domg 8356 fodomr 8380 pwdom 8381 php 8413 isinf 8442 finsschain 8542 fipwuni 8601 fipwss 8604 wdompwdom 8752 inf3lemd 8801 inf3lem1 8802 cantnfle 8845 tc0 8900 r1val1 8926 alephgeom 9218 infmap2 9355 cfub 9386 cf0 9388 cflecard 9390 cfle 9391 fin23lem16 9472 itunitc1 9557 ttukeylem6 9651 ttukeylem7 9652 canthwe 9788 wun0 9855 tsk0 9900 gruina 9955 grur1a 9956 uzssz 11988 xrsup0 12441 fzoss1 12790 fsuppmapnn0fiubex 13086 swrd00 13704 swrdlend 13718 swrd0 13723 repswswrd 13900 xptrrel 14098 sum0 14829 fsumss 14833 fsumcvg3 14837 prod0 15046 0bits 15534 sadid1 15563 sadid2 15564 smu01lem 15580 smu01 15581 smu02 15582 lcmf0 15720 vdwmc2 16054 vdwlem13 16068 ramz2 16099 strfvss 16245 ressbasss 16295 ress0 16297 ismred2 16616 acsfn 16672 acsfn0 16673 0ssc 16849 fullfunc 16918 fthfunc 16919 mrelatglb0 17538 cntzssv 18111 symgsssg 18237 efgsfo 18504 dprdsn 18789 lsp0 19368 lss0v 19375 lspsnat 19505 lsppratlem3 19510 lbsexg 19525 resspsrbas 19776 psr1crng 19917 psr1assa 19918 psr1tos 19919 psr1bas2 19920 vr1cl2 19923 ply1lss 19926 ply1subrg 19927 psr1plusg 19952 psr1vsca 19953 psr1mulr 19954 psr1ring 19977 psr1lmod 19979 psr1sca 19980 evpmss 20291 ocv0 20384 ocvz 20385 css1 20397 0opn 21079 toponsspwpw 21097 basdif0 21128 baspartn 21129 0cld 21213 ntr0 21256 cmpfi 21582 refun0 21689 xkouni 21773 xkoccn 21793 alexsubALTlem2 22222 ptcmplem2 22227 tsmsfbas 22301 setsmstopn 22653 restmetu 22745 tngtopn 22824 iccntr 22994 xrge0gsumle 23006 xrge0tsms 23007 metdstri 23024 ovol0 23659 0mbl 23705 itg1le 23879 itgioo 23981 limcnlp 24041 dvbsss 24065 plyssc 24355 fsumharmonic 25151 egrsubgr 26574 0grsubgr 26575 0uhgrsubgr 26576 chocnul 28731 span0 28945 chsup0 28951 ssnnssfz 30085 xrge0tsmsd 30319 ddemeas 30833 dya2iocuni 30879 oms0 30893 0elcarsg 30903 eulerpartlemt 30967 bnj1143 31396 mrsubrn 31945 msubrn 31961 mthmpps 32014 dfpo2 32176 trpredlem1 32254 nulsslt 32436 nulssgt 32437 bj-nuliotaALT 33535 bj-restsn0 33554 bj-restsn10 33555 bj-ismooredr2 33581 mblfinlem2 33984 mblfinlem3 33985 ismblfin 33987 sstotbnd2 34108 isbnd3 34118 ssbnd 34122 heiborlem6 34150 lub0N 35257 glb0N 35261 0psubN 35817 padd01 35879 padd02 35880 pol0N 35977 pcl0N 35990 0psubclN 36011 mzpcompact2lem 38151 itgocn 38570 fvnonrel 38737 clcnvlem 38764 cnvrcl0 38766 cnvtrcl0 38767 0he 38909 ntrclskb 39200 founiiun0 40178 uzfissfz 40332 limcdm0 40638 cncfiooicc 40895 itgvol0 40971 ibliooicc 40974 ovn0 41567 sprssspr 42571 ssnn0ssfz 42967 setrec2fun 43327 |
Copyright terms: Public domain | W3C validator |