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

Theorem 0ss 3644
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 3620 . . 3  |-  -.  x  e.  (/)
21pm2.21i 126 . 2  |-  ( x  e.  (/)  ->  x  e.  A )
32ssriv 3341 1  |-  (/)  C_  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1728    C_ wss 3309   (/)c0 3616
This theorem is referenced by:  ss0b  3645  0pss  3693  npss0  3694  ssdifeq0  3738  pwpw0  3975  sssn  3986  sspr  3991  sstp  3992  pwsnALT  4039  uni0  4071  int0el  4110  0disj  4236  disjx0  4238  tr0  4344  0elpw  4404  on0eqel  4734  rel0  5034  0ima  5255  dmxpss  5335  dmsnopss  5377  iotassuni  5469  fun0  5543  fresaunres2  5650  f0  5662  fvmptss  5849  fvmptss2  5860  funressn  5955  frxp  6492  riotassuni  6624  oaword1  6831  oaword2  6832  omwordri  6851  oewordri  6871  oeworde  6872  nnaword1  6908  map0e  7087  0domg  7270  fodomr  7294  pwdom  7295  php  7327  isinf  7358  finsschain  7449  fipwuni  7467  fipwss  7470  wdompwdom  7582  inf3lemd  7618  inf3lem1  7619  cantnfle  7662  tc0  7722  r1val1  7748  alephgeom  8001  infmap2  8136  cfub  8167  cf0  8169  cflecard  8171  cfle  8172  fin23lem16  8253  itunitc1  8338  ttukeylem6  8432  ttukeylem7  8433  canthwe  8564  wun0  8631  tsk0  8676  gruina  8731  grur1a  8732  uzssz  10543  xrsup0  10940  fzoss1  11200  swrd00  11803  sum0  12553  fsumss  12557  fsumcvg3  12561  0bits  12989  sadid1  13018  sadid2  13019  smu01lem  13035  smu01  13036  smu02  13037  vdwmc2  13385  vdwlem13  13399  ramz2  13430  strfvss  13525  ressbasss  13559  ress0  13561  strlemor0  13593  ismred2  13866  acsfn  13922  acsfn0  13923  fullfunc  14141  fthfunc  14142  mrelatglb0  14649  cntzssv  15165  efgsfo  15409  dprdsn  15632  lsp0  16123  lss0v  16130  lspsnat  16255  lsppratlem3  16259  lbsexg  16274  resspsrbas  16516  psr1crng  16623  psr1assa  16624  psr1tos  16625  psr1bas2  16626  vr1cl2  16629  ply1lss  16632  ply1subrg  16633  psr1plusg  16654  psr1vsca  16655  psr1mulr  16656  psr1rng  16679  psr1lmod  16681  psr1sca  16682  ocv0  16942  ocvz  16943  css1  16955  0opn  17015  basdif0  17056  baspartn  17057  0cld  17140  cls0  17182  ntr0  17183  cmpfi  17509  xkouni  17669  xkoccn  17689  filcon  17953  alexsubALTlem2  18117  ptcmplem2  18122  tsmsfbas  18195  setsmstopn  18546  restmetu  18655  tngtopn  18729  iccntr  18890  xrge0gsumle  18902  xrge0tsms  18903  metdstri  18919  ovol0  19427  0mbl  19472  itg1le  19641  itgioo  19743  limcnlp  19803  dvbsss  19827  plyssc  20157  fsumharmonic  20888  chocnul  22868  span0  23082  chsup0  23088  ssnnssfz  24183  xrge0tsmsd  24258  dya2iocuni  24668  prod0  25304  dfpo2  25413  trpredlem1  25540  mblfinlem2  26284  mblfinlem3  26285  ismblfin  26287  sstotbnd2  26525  isbnd3  26535  ssbnd  26539  heiborlem6  26567  mzpcompact2lem  26920  itgocn  27458  symgsssg  27497  swrdltnd  28313  bnj1143  29335  lub0N  30161  glb0N  30165  0psubN  30720  padd01  30782  padd02  30783  pol0N  30880  pcl0N  30893  0psubclN  30914
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-v 2967  df-dif 3312  df-in 3316  df-ss 3323  df-nul 3617
  Copyright terms: Public domain W3C validator