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

Theorem 0ss 3483
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 3459 . . 3  |-  -.  x  e.  (/)
21pm2.21i 123 . 2  |-  ( x  e.  (/)  ->  x  e.  A )
32ssriv 3184 1  |-  (/)  C_  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1684    C_ wss 3152   (/)c0 3455
This theorem is referenced by:  ss0b  3484  0pss  3492  npss0  3493  ssdifeq0  3536  pwpw0  3763  sssn  3772  sspr  3777  sstp  3778  pwsnALT  3822  uni0  3854  int0el  3893  0disj  4016  disjx0  4018  tr0  4124  0elpw  4180  on0eqel  4510  rel0  4810  0ima  5031  dmxpss  5107  dmsnopss  5145  iotassuni  5235  fun0  5307  fresaunres2  5413  f0  5425  fvmptss  5609  fvmptss2  5619  funressn  5706  frxp  6225  riotassuni  6343  oaword1  6550  oaword2  6551  omwordri  6570  oewordri  6590  oeworde  6591  nnaword1  6627  map0e  6805  0domg  6988  fodomr  7012  pwdom  7013  php  7045  isinf  7076  finsschain  7162  fipwuni  7179  fipwss  7182  wdompwdom  7292  inf3lemd  7328  inf3lem1  7329  cantnfle  7372  tc0  7432  r1val1  7458  alephgeom  7709  infmap2  7844  cfub  7875  cf0  7877  cflecard  7879  cfle  7880  fin23lem16  7961  itunitc1  8046  ttukeylem6  8141  ttukeylem7  8142  canthwe  8273  wun0  8340  tsk0  8385  gruina  8440  grur1a  8441  uzssz  10247  xrsup0  10642  fzoss1  10896  swrd00  11451  sum0  12194  fsumss  12198  fsumcvg3  12202  0bits  12630  sadid1  12659  sadid2  12660  smu01lem  12676  smu01  12677  smu02  12678  vdwmc2  13026  vdwlem13  13040  ramz2  13071  strfvss  13166  ressbasss  13200  ress0  13202  strlemor0  13234  ismred2  13505  acsfn  13561  acsfn0  13562  fullfunc  13780  fthfunc  13781  mrelatglb0  14288  cntzssv  14804  efgsfo  15048  dprdsn  15271  lsp0  15766  lss0v  15773  lspsnat  15898  lsppratlem3  15902  lbsexg  15917  resspsrbas  16159  psr1crng  16266  psr1assa  16267  psr1tos  16268  psr1bas2  16269  vr1cl2  16272  ply1lss  16275  ply1subrg  16276  psr1plusg  16300  psr1vsca  16301  psr1mulr  16302  psr1rng  16325  psr1lmod  16327  psr1sca  16328  ocv0  16577  ocvz  16578  css1  16590  0opn  16650  basdif0  16691  baspartn  16692  0cld  16775  cls0  16817  ntr0  16818  cmpfi  17135  xkouni  17294  xkoccn  17313  filcon  17578  alexsubALTlem2  17742  ptcmplem2  17747  tsmsfbas  17810  setsmstopn  18024  tngtopn  18166  iccntr  18326  xrge0gsumle  18338  xrge0tsms  18339  metdstri  18355  ovol0  18852  0mbl  18897  itg1le  19068  itgioo  19170  limcnlp  19228  dvbsss  19252  plyssc  19582  fsumharmonic  20305  chocnul  21907  span0  22121  chsup0  22127  ssnnssfz  23277  xrge0tsmsd  23382  dfpo2  24112  trpredlem1  24230  imfstnrelc  25081  oibbi1  25509  oibbi2  25510  sallnei  25529  efilcp  25552  sstotbnd2  26498  isbnd3  26508  ssbnd  26512  heiborlem6  26540  mzpcompact2lem  26829  itgocn  27369  symgsssg  27408  bnj1143  28822  lub0N  29379  glb0N  29383  0psubN  29938  padd01  30000  padd02  30001  pol0N  30098  pcl0N  30111  0psubclN  30132
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-dif 3155  df-in 3159  df-ss 3166  df-nul 3456
  Copyright terms: Public domain W3C validator