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

Theorem 0ss 3643
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 3619 . . 3  |-  -.  x  e.  (/)
21pm2.21i 125 . 2  |-  ( x  e.  (/)  ->  x  e.  A )
32ssriv 3339 1  |-  (/)  C_  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1725    C_ wss 3307   (/)c0 3615
This theorem is referenced by:  ss0b  3644  0pss  3652  npss0  3653  ssdifeq0  3697  pwpw0  3933  sssn  3944  sspr  3949  sstp  3950  pwsnALT  3997  uni0  4029  int0el  4068  0disj  4192  disjx0  4194  tr0  4300  0elpw  4356  on0eqel  4685  rel0  4985  0ima  5208  dmxpss  5286  dmsnopss  5328  iotassuni  5420  fun0  5494  fresaunres2  5601  f0  5613  fvmptss  5799  fvmptss2  5810  funressn  5905  frxp  6442  riotassuni  6574  oaword1  6781  oaword2  6782  omwordri  6801  oewordri  6821  oeworde  6822  nnaword1  6858  map0e  7037  0domg  7220  fodomr  7244  pwdom  7245  php  7277  isinf  7308  finsschain  7399  fipwuni  7417  fipwss  7420  wdompwdom  7530  inf3lemd  7566  inf3lem1  7567  cantnfle  7610  tc0  7670  r1val1  7696  alephgeom  7947  infmap2  8082  cfub  8113  cf0  8115  cflecard  8117  cfle  8118  fin23lem16  8199  itunitc1  8284  ttukeylem6  8378  ttukeylem7  8379  canthwe  8510  wun0  8577  tsk0  8622  gruina  8677  grur1a  8678  uzssz  10489  xrsup0  10886  fzoss1  11145  swrd00  11748  sum0  12498  fsumss  12502  fsumcvg3  12506  0bits  12934  sadid1  12963  sadid2  12964  smu01lem  12980  smu01  12981  smu02  12982  vdwmc2  13330  vdwlem13  13344  ramz2  13375  strfvss  13470  ressbasss  13504  ress0  13506  strlemor0  13538  ismred2  13811  acsfn  13867  acsfn0  13868  fullfunc  14086  fthfunc  14087  mrelatglb0  14594  cntzssv  15110  efgsfo  15354  dprdsn  15577  lsp0  16068  lss0v  16075  lspsnat  16200  lsppratlem3  16204  lbsexg  16219  resspsrbas  16461  psr1crng  16568  psr1assa  16569  psr1tos  16570  psr1bas2  16571  vr1cl2  16574  ply1lss  16577  ply1subrg  16578  psr1plusg  16599  psr1vsca  16600  psr1mulr  16601  psr1rng  16624  psr1lmod  16626  psr1sca  16627  ocv0  16887  ocvz  16888  css1  16900  0opn  16960  basdif0  17001  baspartn  17002  0cld  17085  cls0  17127  ntr0  17128  cmpfi  17454  xkouni  17614  xkoccn  17634  filcon  17898  alexsubALTlem2  18062  ptcmplem2  18067  tsmsfbas  18140  setsmstopn  18491  restmetu  18600  tngtopn  18674  iccntr  18835  xrge0gsumle  18847  xrge0tsms  18848  metdstri  18864  ovol0  19372  0mbl  19417  itg1le  19588  itgioo  19690  limcnlp  19748  dvbsss  19772  plyssc  20102  fsumharmonic  20833  chocnul  22813  span0  23027  chsup0  23033  ssnnssfz  24131  xrge0tsmsd  24206  dya2iocuni  24616  prod0  25253  dfpo2  25362  trpredlem1  25480  mblfinlem  26185  mblfinlem2  26186  ismblfin  26188  sstotbnd2  26415  isbnd3  26425  ssbnd  26429  heiborlem6  26457  mzpcompact2lem  26740  itgocn  27279  symgsssg  27318  swrdltnd  28042  bnj1143  28913  lub0N  29718  glb0N  29722  0psubN  30277  padd01  30339  padd02  30340  pol0N  30437  pcl0N  30450  0psubclN  30471
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-v 2945  df-dif 3310  df-in 3314  df-ss 3321  df-nul 3616
  Copyright terms: Public domain W3C validator