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

Theorem 0ss 3458
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
StepHypRef Expression
1 noel 3434 . . 3  |-  -.  x  e.  (/)
21pm2.21i 125 . 2  |-  ( x  e.  (/)  ->  x  e.  A )
32ssriv 3159 1  |-  (/)  C_  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1621    C_ wss 3127   (/)c0 3430
This theorem is referenced by:  ss0b  3459  0pss  3467  npss0  3468  ssdifeq0  3511  pwpw0  3737  sssn  3746  sspr  3751  sstp  3752  pwsnALT  3796  uni0  3828  int0el  3867  0disj  3990  disjx0  3992  tr0  4098  0elpw  4152  on0eqel  4482  rel0  4798  0ima  5019  dmxpss  5095  dmsnopss  5132  fun0  5245  fresaunres2  5351  f0  5363  fvmptss  5543  fvmptss2  5553  funressn  5640  frxp  6159  iotassuni  6241  riotassuni  6311  oaword1  6518  oaword2  6519  omwordri  6538  oewordri  6558  oeworde  6559  nnaword1  6595  map0e  6773  0domg  6956  fodomr  6980  pwdom  6981  php  7013  isinf  7044  finsschain  7130  fipwuni  7147  fipwss  7150  wdompwdom  7260  inf3lemd  7296  inf3lem1  7297  cantnfle  7340  tc0  7400  r1val1  7426  alephgeom  7677  infmap2  7812  cfub  7843  cf0  7845  cflecard  7847  cfle  7848  fin23lem16  7929  itunitc1  8014  ttukeylem6  8109  ttukeylem7  8110  canthwe  8241  wun0  8308  tsk0  8353  gruina  8408  grur1a  8409  uzssz  10214  xrsup0  10608  fzoss1  10862  swrd00  11416  sum0  12159  fsumss  12163  fsumcvg3  12167  0bits  12592  sadid1  12621  sadid2  12622  smu01lem  12638  smu01  12639  smu02  12640  vdwmc2  12988  vdwlem13  13002  ramz2  13033  strfvss  13128  ressbasss  13162  ress0  13164  strlemor0  13196  ismred2  13467  acsfn  13523  acsfn0  13524  fullfunc  13742  fthfunc  13743  mrelatglb0  14250  cntzssv  14766  efgsfo  15010  dprdsn  15233  lsp0  15728  lss0v  15735  lspsnat  15860  lsppratlem3  15864  lbsexg  15879  resspsrbas  16121  psr1crng  16228  psr1assa  16229  psr1tos  16230  psr1bas2  16231  vr1cl2  16234  ply1lss  16237  ply1subrg  16238  psr1plusg  16262  psr1vsca  16263  psr1mulr  16264  psr1rng  16287  psr1lmod  16289  psr1sca  16290  ocv0  16539  ocvz  16540  css1  16552  0opn  16612  basdif0  16653  baspartn  16654  0cld  16737  cls0  16779  ntr0  16780  cmpfi  17097  xkouni  17256  xkoccn  17275  filcon  17540  alexsubALTlem2  17704  ptcmplem2  17709  tsmsfbas  17772  setsmstopn  17986  tngtopn  18128  iccntr  18288  xrge0gsumle  18300  xrge0tsms  18301  metdstri  18317  ovol0  18814  0mbl  18859  itg1le  19030  itgioo  19132  limcnlp  19190  dvbsss  19214  plyssc  19544  fsumharmonic  20267  chocnul  21867  span0  22081  chsup0  22087  dfpo2  23483  trpredlem1  23599  imfstnrelc  24447  oibbi1  24876  oibbi2  24877  sallnei  24896  efilcp  24919  sstotbnd2  25865  isbnd3  25875  ssbnd  25879  heiborlem6  25907  mzpcompact2lem  26196  itgocn  26736  symgsssg  26775  bnj1143  27871  lub0N  28546  glb0N  28550  0psubN  29105  padd01  29167  padd02  29168  pol0N  29265  pcl0N  29278  0psubclN  29299
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-v 2765  df-dif 3130  df-in 3134  df-ss 3141  df-nul 3431
  Copyright terms: Public domain W3C validator