MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  0ss Unicode version

Theorem 0ss 3496
Description: The null set is a subset of any class. Part of Exercise 1 of [TakeutiZaring] p. 22. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
0ss  |-  (/)  C_  A

Proof of Theorem 0ss
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 noel 3472 . . 3  |-  -.  x  e.  (/)
21pm2.21i 123 . 2  |-  ( x  e.  (/)  ->  x  e.  A )
32ssriv 3197 1  |-  (/)  C_  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1696    C_ wss 3165   (/)c0 3468
This theorem is referenced by:  ss0b  3497  0pss  3505  npss0  3506  ssdifeq0  3549  pwpw0  3779  sssn  3788  sspr  3793  sstp  3794  pwsnALT  3838  uni0  3870  int0el  3909  0disj  4032  disjx0  4034  tr0  4140  0elpw  4196  on0eqel  4526  rel0  4826  0ima  5047  dmxpss  5123  dmsnopss  5161  iotassuni  5251  fun0  5323  fresaunres2  5429  f0  5441  fvmptss  5625  fvmptss2  5635  funressn  5722  frxp  6241  riotassuni  6359  oaword1  6566  oaword2  6567  omwordri  6586  oewordri  6606  oeworde  6607  nnaword1  6643  map0e  6821  0domg  7004  fodomr  7028  pwdom  7029  php  7061  isinf  7092  finsschain  7178  fipwuni  7195  fipwss  7198  wdompwdom  7308  inf3lemd  7344  inf3lem1  7345  cantnfle  7388  tc0  7448  r1val1  7474  alephgeom  7725  infmap2  7860  cfub  7891  cf0  7893  cflecard  7895  cfle  7896  fin23lem16  7977  itunitc1  8062  ttukeylem6  8157  ttukeylem7  8158  canthwe  8289  wun0  8356  tsk0  8401  gruina  8456  grur1a  8457  uzssz  10263  xrsup0  10658  fzoss1  10912  swrd00  11467  sum0  12210  fsumss  12214  fsumcvg3  12218  0bits  12646  sadid1  12675  sadid2  12676  smu01lem  12692  smu01  12693  smu02  12694  vdwmc2  13042  vdwlem13  13056  ramz2  13087  strfvss  13182  ressbasss  13216  ress0  13218  strlemor0  13250  ismred2  13521  acsfn  13577  acsfn0  13578  fullfunc  13796  fthfunc  13797  mrelatglb0  14304  cntzssv  14820  efgsfo  15064  dprdsn  15287  lsp0  15782  lss0v  15789  lspsnat  15914  lsppratlem3  15918  lbsexg  15933  resspsrbas  16175  psr1crng  16282  psr1assa  16283  psr1tos  16284  psr1bas2  16285  vr1cl2  16288  ply1lss  16291  ply1subrg  16292  psr1plusg  16316  psr1vsca  16317  psr1mulr  16318  psr1rng  16341  psr1lmod  16343  psr1sca  16344  ocv0  16593  ocvz  16594  css1  16606  0opn  16666  basdif0  16707  baspartn  16708  0cld  16791  cls0  16833  ntr0  16834  cmpfi  17151  xkouni  17310  xkoccn  17329  filcon  17594  alexsubALTlem2  17758  ptcmplem2  17763  tsmsfbas  17826  setsmstopn  18040  tngtopn  18182  iccntr  18342  xrge0gsumle  18354  xrge0tsms  18355  metdstri  18371  ovol0  18868  0mbl  18913  itg1le  19084  itgioo  19186  limcnlp  19244  dvbsss  19268  plyssc  19598  fsumharmonic  20321  chocnul  21923  span0  22137  chsup0  22143  ssnnssfz  23292  xrge0tsmsd  23397  cprod0  24168  dfpo2  24183  trpredlem1  24301  imfstnrelc  25184  oibbi1  25612  oibbi2  25613  sallnei  25632  efilcp  25655  sstotbnd2  26601  isbnd3  26611  ssbnd  26615  heiborlem6  26643  mzpcompact2lem  26932  itgocn  27472  symgsssg  27511  bnj1143  29138  lub0N  30001  glb0N  30005  0psubN  30560  padd01  30622  padd02  30623  pol0N  30720  pcl0N  30733  0psubclN  30754
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-dif 3168  df-in 3172  df-ss 3179  df-nul 3469
  Copyright terms: Public domain W3C validator