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

Theorem 0ss 3484
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 3460 . . 3  |-  -.  x  e.  (/)
21pm2.21i 125 . 2  |-  ( x  e.  (/)  ->  x  e.  A )
32ssriv 3185 1  |-  (/)  C_  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1688    C_ wss 3153   (/)c0 3456
This theorem is referenced by:  ss0b  3485  0pss  3493  npss0  3494  ssdifeq0  3537  pwpw0  3764  sssn  3773  sspr  3778  sstp  3779  pwsnALT  3823  uni0  3855  int0el  3894  0disj  4017  disjx0  4019  tr0  4125  0elpw  4179  on0eqel  4509  rel0  4809  0ima  5030  dmxpss  5106  dmsnopss  5143  fun0  5272  fresaunres2  5378  f0  5390  fvmptss  5570  fvmptss2  5580  funressn  5667  frxp  6186  iotassuni  6268  riotassuni  6338  oaword1  6545  oaword2  6546  omwordri  6565  oewordri  6585  oeworde  6586  nnaword1  6622  map0e  6800  0domg  6983  fodomr  7007  pwdom  7008  php  7040  isinf  7071  finsschain  7157  fipwuni  7174  fipwss  7177  wdompwdom  7287  inf3lemd  7323  inf3lem1  7324  cantnfle  7367  tc0  7427  r1val1  7453  alephgeom  7704  infmap2  7839  cfub  7870  cf0  7872  cflecard  7874  cfle  7875  fin23lem16  7956  itunitc1  8041  ttukeylem6  8136  ttukeylem7  8137  canthwe  8268  wun0  8335  tsk0  8380  gruina  8435  grur1a  8436  uzssz  10242  xrsup0  10636  fzoss1  10890  swrd00  11445  sum0  12188  fsumss  12192  fsumcvg3  12196  0bits  12624  sadid1  12653  sadid2  12654  smu01lem  12670  smu01  12671  smu02  12672  vdwmc2  13020  vdwlem13  13034  ramz2  13065  strfvss  13160  ressbasss  13194  ress0  13196  strlemor0  13228  ismred2  13499  acsfn  13555  acsfn0  13556  fullfunc  13774  fthfunc  13775  mrelatglb0  14282  cntzssv  14798  efgsfo  15042  dprdsn  15265  lsp0  15760  lss0v  15767  lspsnat  15892  lsppratlem3  15896  lbsexg  15911  resspsrbas  16153  psr1crng  16260  psr1assa  16261  psr1tos  16262  psr1bas2  16263  vr1cl2  16266  ply1lss  16269  ply1subrg  16270  psr1plusg  16294  psr1vsca  16295  psr1mulr  16296  psr1rng  16319  psr1lmod  16321  psr1sca  16322  ocv0  16571  ocvz  16572  css1  16584  0opn  16644  basdif0  16685  baspartn  16686  0cld  16769  cls0  16811  ntr0  16812  cmpfi  17129  xkouni  17288  xkoccn  17307  filcon  17572  alexsubALTlem2  17736  ptcmplem2  17741  tsmsfbas  17804  setsmstopn  18018  tngtopn  18160  iccntr  18320  xrge0gsumle  18332  xrge0tsms  18333  metdstri  18349  ovol0  18846  0mbl  18891  itg1le  19062  itgioo  19164  limcnlp  19222  dvbsss  19246  plyssc  19576  fsumharmonic  20299  chocnul  21899  span0  22113  chsup0  22119  dfpo2  23515  trpredlem1  23631  imfstnrelc  24479  oibbi1  24908  oibbi2  24909  sallnei  24928  efilcp  24951  sstotbnd2  25897  isbnd3  25907  ssbnd  25911  heiborlem6  25939  mzpcompact2lem  26228  itgocn  26768  symgsssg  26807  bnj1143  28089  lub0N  28646  glb0N  28650  0psubN  29205  padd01  29267  padd02  29268  pol0N  29365  pcl0N  29378  0psubclN  29399
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-6 1707  ax-7 1712  ax-11 1719  ax-12 1869  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1534  df-nf 1537  df-sb 1636  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-dif 3156  df-in 3160  df-ss 3167  df-nul 3457
  Copyright terms: Public domain W3C validator