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

Theorem 0ss 3390
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 3366 . . 3  |-  -.  x  e.  (/)
21pm2.21i 125 . 2  |-  ( x  e.  (/)  ->  x  e.  A )
32ssriv 3105 1  |-  (/)  C_  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1621    C_ wss 3078   (/)c0 3362
This theorem is referenced by:  ss0b  3391  0pss  3399  npss0  3400  ssdifeq0  3442  pwpw0  3663  sssn  3672  sspr  3677  sstp  3678  pwsnALT  3722  uni0  3752  int0el  3791  0disj  3913  disjx0  3915  tr0  4021  0elpw  4074  on0eqel  4401  rel0  4717  0ima  4938  dmxpss  5014  dmsnopss  5051  fun0  5164  fresaunres2  5270  f0  5282  fvmptss  5461  fvmptss2  5471  funressn  5558  frxp  6077  iotassuni  6159  riotassuni  6229  oaword1  6436  oaword2  6437  omwordri  6456  oewordri  6476  oeworde  6477  nnaword1  6513  map0e  6691  0domg  6873  fodomr  6897  pwdom  6898  php  6930  isinf  6961  finsschain  7046  fipwuni  7063  fipwss  7066  wdompwdom  7176  inf3lemd  7212  inf3lem1  7213  cantnfle  7256  tc0  7316  r1val1  7342  alephgeom  7593  infmap2  7728  cfub  7759  cf0  7761  cflecard  7763  cfle  7764  fin23lem16  7845  itunitc1  7930  ttukeylem6  8025  ttukeylem7  8026  canthwe  8153  wun0  8220  tsk0  8265  gruina  8320  grur1a  8321  uzssz  10126  xrsup0  10520  fzoss1  10774  swrd00  11328  sum0  12071  fsumss  12075  fsumcvg3  12079  0bits  12504  sadid1  12533  sadid2  12534  smu01lem  12550  smu01  12551  smu02  12552  vdwmc2  12900  vdwlem13  12914  ramz2  12945  strfvss  13040  ressbasss  13074  ress0  13076  strlemor0  13108  ismred2  13377  acsfn  13405  acsfn0  13406  fullfunc  13624  fthfunc  13625  mrelatglb0  14123  cntzssv  14639  efgsfo  14883  dprdsn  15106  lsp0  15601  lss0v  15608  lspsnat  15732  lsppratlem3  15736  lbsexg  15749  resspsrbas  15991  psr1crng  16098  psr1assa  16099  psr1tos  16100  psr1bas2  16101  vr1cl2  16104  ply1lss  16107  ply1subrg  16108  psr1plusg  16132  psr1vsca  16133  psr1mulr  16134  psr1rng  16157  psr1lmod  16159  psr1sca  16160  ocv0  16409  ocvz  16410  css1  16422  0opn  16482  basdif0  16523  baspartn  16524  0cld  16607  cls0  16649  ntr0  16650  cmpfi  16967  xkouni  17126  xkoccn  17145  filcon  17410  alexsubALTlem2  17574  ptcmplem2  17579  tsmsfbas  17642  setsmstopn  17856  tngtopn  17998  iccntr  18158  xrge0gsumle  18170  xrge0tsms  18171  metdstri  18187  ovol0  18684  0mbl  18729  itg1le  18900  itgioo  19002  limcnlp  19060  dvbsss  19084  plyssc  19414  fsumharmonic  20137  chocnul  21737  span0  21951  chsup0  21957  dfpo2  23282  trpredlem1  23398  imfstnrelc  24246  oibbi1  24675  oibbi2  24676  sallnei  24695  efilcp  24718  sstotbnd2  25664  isbnd3  25674  ssbnd  25678  heiborlem6  25706  mzpcompact2lem  25995  itgocn  26535  symgsssg  26574  bnj1143  27608  lub0N  28283  glb0N  28287  0psubN  28842  padd01  28904  padd02  28905  pol0N  29002  pcl0N  29015  0psubclN  29036
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 1926  ax-ext 2234
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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-dif 3081  df-in 3085  df-ss 3089  df-nul 3363
  Copyright terms: Public domain W3C validator