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

Theorem 0ss 3616
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 3592 . . 3  |-  -.  x  e.  (/)
21pm2.21i 125 . 2  |-  ( x  e.  (/)  ->  x  e.  A )
32ssriv 3312 1  |-  (/)  C_  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1721    C_ wss 3280   (/)c0 3588
This theorem is referenced by:  ss0b  3617  0pss  3625  npss0  3626  ssdifeq0  3670  pwpw0  3906  sssn  3917  sspr  3922  sstp  3923  pwsnALT  3970  uni0  4002  int0el  4041  0disj  4165  disjx0  4167  tr0  4273  0elpw  4329  on0eqel  4658  rel0  4958  0ima  5181  dmxpss  5259  dmsnopss  5301  iotassuni  5393  fun0  5467  fresaunres2  5574  f0  5586  fvmptss  5772  fvmptss2  5783  funressn  5878  frxp  6415  riotassuni  6547  oaword1  6754  oaword2  6755  omwordri  6774  oewordri  6794  oeworde  6795  nnaword1  6831  map0e  7010  0domg  7193  fodomr  7217  pwdom  7218  php  7250  isinf  7281  finsschain  7371  fipwuni  7389  fipwss  7392  wdompwdom  7502  inf3lemd  7538  inf3lem1  7539  cantnfle  7582  tc0  7642  r1val1  7668  alephgeom  7919  infmap2  8054  cfub  8085  cf0  8087  cflecard  8089  cfle  8090  fin23lem16  8171  itunitc1  8256  ttukeylem6  8350  ttukeylem7  8351  canthwe  8482  wun0  8549  tsk0  8594  gruina  8649  grur1a  8650  uzssz  10461  xrsup0  10858  fzoss1  11117  swrd00  11720  sum0  12470  fsumss  12474  fsumcvg3  12478  0bits  12906  sadid1  12935  sadid2  12936  smu01lem  12952  smu01  12953  smu02  12954  vdwmc2  13302  vdwlem13  13316  ramz2  13347  strfvss  13442  ressbasss  13476  ress0  13478  strlemor0  13510  ismred2  13783  acsfn  13839  acsfn0  13840  fullfunc  14058  fthfunc  14059  mrelatglb0  14566  cntzssv  15082  efgsfo  15326  dprdsn  15549  lsp0  16040  lss0v  16047  lspsnat  16172  lsppratlem3  16176  lbsexg  16191  resspsrbas  16433  psr1crng  16540  psr1assa  16541  psr1tos  16542  psr1bas2  16543  vr1cl2  16546  ply1lss  16549  ply1subrg  16550  psr1plusg  16571  psr1vsca  16572  psr1mulr  16573  psr1rng  16596  psr1lmod  16598  psr1sca  16599  ocv0  16859  ocvz  16860  css1  16872  0opn  16932  basdif0  16973  baspartn  16974  0cld  17057  cls0  17099  ntr0  17100  cmpfi  17425  xkouni  17584  xkoccn  17604  filcon  17868  alexsubALTlem2  18032  ptcmplem2  18037  tsmsfbas  18110  setsmstopn  18461  restmetu  18570  tngtopn  18644  iccntr  18805  xrge0gsumle  18817  xrge0tsms  18818  metdstri  18834  ovol0  19342  0mbl  19387  itg1le  19558  itgioo  19660  limcnlp  19718  dvbsss  19742  plyssc  20072  fsumharmonic  20803  chocnul  22783  span0  22997  chsup0  23003  ssnnssfz  24101  xrge0tsmsd  24176  dya2iocuni  24586  prod0  25222  dfpo2  25326  trpredlem1  25444  mblfinlem  26143  mblfinlem2  26144  ismblfin  26146  sstotbnd2  26373  isbnd3  26383  ssbnd  26387  heiborlem6  26415  mzpcompact2lem  26698  itgocn  27237  symgsssg  27276  swrdltnd  28000  bnj1143  28867  lub0N  29672  glb0N  29676  0psubN  30231  padd01  30293  padd02  30294  pol0N  30391  pcl0N  30404  0psubclN  30425
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-dif 3283  df-in 3287  df-ss 3294  df-nul 3589
  Copyright terms: Public domain W3C validator