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

Theorem 0ss 3592
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 3568 . . 3  |-  -.  x  e.  (/)
21pm2.21i 125 . 2  |-  ( x  e.  (/)  ->  x  e.  A )
32ssriv 3288 1  |-  (/)  C_  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1717    C_ wss 3256   (/)c0 3564
This theorem is referenced by:  ss0b  3593  0pss  3601  npss0  3602  ssdifeq0  3646  pwpw0  3882  sssn  3893  sspr  3898  sstp  3899  pwsnALT  3945  uni0  3977  int0el  4016  0disj  4139  disjx0  4141  tr0  4247  0elpw  4303  on0eqel  4632  rel0  4932  0ima  5155  dmxpss  5233  dmsnopss  5275  iotassuni  5367  fun0  5441  fresaunres2  5548  f0  5560  fvmptss  5745  fvmptss2  5756  funressn  5851  frxp  6385  riotassuni  6517  oaword1  6724  oaword2  6725  omwordri  6744  oewordri  6764  oeworde  6765  nnaword1  6801  map0e  6980  0domg  7163  fodomr  7187  pwdom  7188  php  7220  isinf  7251  finsschain  7341  fipwuni  7359  fipwss  7362  wdompwdom  7472  inf3lemd  7508  inf3lem1  7509  cantnfle  7552  tc0  7612  r1val1  7638  alephgeom  7889  infmap2  8024  cfub  8055  cf0  8057  cflecard  8059  cfle  8060  fin23lem16  8141  itunitc1  8226  ttukeylem6  8320  ttukeylem7  8321  canthwe  8452  wun0  8519  tsk0  8564  gruina  8619  grur1a  8620  uzssz  10430  xrsup0  10827  fzoss1  11085  swrd00  11685  sum0  12435  fsumss  12439  fsumcvg3  12443  0bits  12871  sadid1  12900  sadid2  12901  smu01lem  12917  smu01  12918  smu02  12919  vdwmc2  13267  vdwlem13  13281  ramz2  13312  strfvss  13407  ressbasss  13441  ress0  13443  strlemor0  13475  ismred2  13748  acsfn  13804  acsfn0  13805  fullfunc  14023  fthfunc  14024  mrelatglb0  14531  cntzssv  15047  efgsfo  15291  dprdsn  15514  lsp0  16005  lss0v  16012  lspsnat  16137  lsppratlem3  16141  lbsexg  16156  resspsrbas  16398  psr1crng  16505  psr1assa  16506  psr1tos  16507  psr1bas2  16508  vr1cl2  16511  ply1lss  16514  ply1subrg  16515  psr1plusg  16536  psr1vsca  16537  psr1mulr  16538  psr1rng  16561  psr1lmod  16563  psr1sca  16564  ocv0  16820  ocvz  16821  css1  16833  0opn  16893  basdif0  16934  baspartn  16935  0cld  17018  cls0  17060  ntr0  17061  cmpfi  17386  xkouni  17545  xkoccn  17565  filcon  17829  alexsubALTlem2  17993  ptcmplem2  17998  tsmsfbas  18071  setsmstopn  18391  restmetu  18482  tngtopn  18555  iccntr  18716  xrge0gsumle  18728  xrge0tsms  18729  metdstri  18745  ovol0  19249  0mbl  19294  itg1le  19465  itgioo  19567  limcnlp  19625  dvbsss  19649  plyssc  19979  fsumharmonic  20710  chocnul  22671  span0  22885  chsup0  22891  ssnnssfz  23977  xrge0tsmsd  24045  dya2iocuni  24420  prod0  25041  dfpo2  25129  trpredlem1  25247  sstotbnd2  26167  isbnd3  26177  ssbnd  26181  heiborlem6  26209  mzpcompact2lem  26492  itgocn  27031  symgsssg  27070  bnj1143  28492  lub0N  29355  glb0N  29359  0psubN  29914  padd01  29976  padd02  29977  pol0N  30074  pcl0N  30087  0psubclN  30108
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-v 2894  df-dif 3259  df-in 3263  df-ss 3270  df-nul 3565
  Copyright terms: Public domain W3C validator