Theorem 0ss 4330

Description: The null set is a subset of any class. Part of Exercise 1 of [TakeutiZaring] p. 22. (Contributed by NM, 21-Jun-1993.)

Assertion

Ref	Expression
0ss	⊢ ∅ ⊆ 𝐴

Proof of Theorem 0ss

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		noel 4264	. . 3 ⊢ ¬ 𝑥 ∈ ∅
2	1	pm2.21i 119	. 2 ⊢ (𝑥 ∈ ∅ → 𝑥 ∈ 𝐴)
3	2	ssriv 3925	1 ⊢ ∅ ⊆ 𝐴

Syntax hints:   ∈ wcel 2106   ⊆ wss 3887  ∅c0 4256

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-dif 3890  df-in 3894  df-ss 3904  df-nul 4257

This theorem is referenced by:  ss0b  4331  0pss  4378  npss0  4379  ssdifeq0  4417  pwpw0  4746  sssn  4759  sspr  4766  sstp  4767  pwsnOLD  4832  uni0  4869  int0el  4910  0disj  5066  disjx0  5068  tr0  5202  al0ssb  5232  0elpw  5278  rel0  5709  0ima  5986  dmxpss  6074  dmsnopss  6117  dfpo2  6199  on0eqel  6384  iotassuni  6412  fun0  6499  f0  6655  fvmptss  6887  fvmptss2  6900  funressn  7031  riotassuni  7273  frxp  7967  suppssdm  7993  suppun  8000  suppss  8010  suppssOLD  8011  suppssov1  8014  suppss2  8016  suppssfv  8018  oaword1  8383  oaword2  8384  omwordri  8403  oewordri  8423  oeworde  8424  nnaword1  8460  mapssfset  8639  0domgOLD  8888  fodomr  8915  pwdom  8916  php  8993  phpOLD  9005  isinf  9036  finsschain  9126  fipwuni  9185  fipwss  9188  wdompwdom  9337  inf3lemd  9385  inf3lem1  9386  cantnfle  9429  ttrclselem1  9483  tc0  9505  r1val1  9544  alephgeom  9838  infmap2  9974  cfub  10005  cf0  10007  cflecard  10009  cfle  10010  fin23lem16  10091  itunitc1  10176  ttukeylem6  10270  ttukeylem7  10271  canthwe  10407  wun0  10474  tsk0  10519  gruina  10574  grur1a  10575  uzssz  12603  xrsup0  13057  fzoss1  13414  fsuppmapnn0fiubex  13712  swrd00  14357  swrdlend  14366  repswswrd  14497  xptrrel  14691  relexpdmd  14755  relexprnd  14759  relexpfldd  14761  rtrclreclem4  14772  sum0  15433  fsumss  15437  fsumcvg3  15441  prod0  15653  0bits  16146  sadid1  16175  sadid2  16176  smu01lem  16192  smu01  16193  smu02  16194  lcmf0  16339  vdwmc2  16680  vdwlem13  16694  ramz2  16725  strfvss  16888  ressbasss  16950  ress0  16953  ismred2  17312  acsfn  17368  acsfn0  17369  0ssc  17552  fullfunc  17622  fthfunc  17623  mrelatglb0  18279  cntzssv  18934  symgsssg  19075  efgsfo  19345  dprdsn  19639  lsp0  20271  lss0v  20278  lspsnat  20407  lsppratlem3  20411  lbsexg  20426  evpmss  20791  ocv0  20882  ocvz  20883  css1  20895  resspsrbas  21184  mhp0cl  21336  psr1crng  21358  psr1assa  21359  psr1tos  21360  psr1bas2  21361  vr1cl2  21364  ply1lss  21367  ply1subrg  21368  psr1plusg  21393  psr1vsca  21394  psr1mulr  21395  psr1ring  21418  psr1lmod  21420  psr1sca  21421  0opn  22053  toponsspwpw  22071  basdif0  22103  baspartn  22104  0cld  22189  ntr0  22232  cmpfi  22559  refun0  22666  xkouni  22750  xkoccn  22770  alexsubALTlem2  23199  ptcmplem2  23204  tsmsfbas  23279  setsmstopn  23633  restmetu  23726  tngtopn  23814  iccntr  23984  xrge0gsumle  23996  xrge0tsms  23997  metdstri  24014  ovol0  24657  0mbl  24703  itg1le  24878  itgioo  24980  limcnlp  25042  dvbsss  25066  plyssc  25361  fsumharmonic  26161  egrsubgr  27644  0grsubgr  27645  0uhgrsubgr  27646  chocnul  29690  span0  29904  chsup0  29910  ssnnssfz  31108  xrge0tsmsd  31317  ddemeas  32204  dya2iocuni  32250  oms0  32264  0elcarsg  32274  eulerpartlemt  32338  bnj1143  32770  mrsubrn  33475  msubrn  33491  mthmpps  33544  nulsslt  33991  nulssgt  33992  bday0b  34024  madess  34059  oldssmade  34060  bj-nuliotaALT  35229  bj-restsn0  35256  bj-restsn10  35257  bj-imdirco  35361  pibt2  35588  mblfinlem2  35815  mblfinlem3  35816  ismblfin  35818  sstotbnd2  35932  isbnd3  35942  ssbnd  35946  heiborlem6  35974  lub0N  37203  glb0N  37207  0psubN  37763  padd01  37825  padd02  37826  pol0N  37923  pcl0N  37936  0psubclN  37957  sn-iotassuni  40196  mzpcompact2lem  40573  itgocn  40989  fvnonrel  41205  clcnvlem  41231  cnvrcl0  41233  cnvtrcl0  41234  0he  41390  ntrclskb  41679  gru0eld  41847  mnu0eld  41883  mnuprdlem4  41893  mnuprd  41894  founiiun0  42728  uzfissfz  42865  limcdm0  43159  cncfiooicc  43435  itgvol0  43509  ibliooicc  43512  ovn0  44104  sprssspr  44933  ssnn0ssfz  45685  ipolub0  46278  ipoglb0  46280  setrec2fun  46398