Theorem 0ss 4352

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 4290	. . 3 ⊢ ¬ 𝑥 ∈ ∅
2	1	pm2.21i 119	. 2 ⊢ (𝑥 ∈ ∅ → 𝑥 ∈ 𝐴)
3	2	ssriv 3937	1 ⊢ ∅ ⊆ 𝐴

Syntax hints:   ∈ wcel 2113   ⊆ wss 3901  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-dif 3904  df-ss 3918  df-nul 4286

This theorem is referenced by:  ss0b  4353  0pss  4399  npss0  4400  ssdifeq0  4439  pwpw0  4769  sssn  4782  sspr  4791  sstp  4792  uni0OLD  4892  int0el  4934  0disj  5091  disjx0  5093  tr0  5217  al0ssb  5253  0elpw  5301  rel0  5748  0ima  6037  dmxpss  6129  dmsnopss  6172  dfpo2  6254  on0eqel  6442  iotassuni  6467  fun0  6557  f0  6715  fvmptss  6953  fvmptss2  6967  funressn  7104  riotassuni  7355  ordsuci  7753  frxp  8068  suppssdm  8119  suppun  8126  suppss  8136  suppssov1  8139  suppssov2  8140  suppss2  8142  suppssfv  8144  oaword1  8479  oaword2  8480  omwordri  8499  oewordri  8520  oeworde  8521  nnaword1  8557  naddword1  8619  mapssfset  8788  fodomr  9056  pwdom  9057  php  9131  isinf  9165  fodomfir  9228  finsschain  9259  fipwuni  9329  fipwss  9332  wdompwdom  9483  inf3lemd  9536  inf3lem1  9537  cantnfle  9580  ttrclselem1  9634  tc0  9654  r1val1  9698  alephgeom  9992  infmap2  10127  cfub  10159  cf0  10161  cflecard  10163  cfle  10164  fin23lem16  10245  itunitc1  10330  ttukeylem6  10424  ttukeylem7  10425  canthwe  10562  wun0  10629  tsk0  10674  gruina  10729  grur1a  10730  uzssz  12772  xrsup0  13238  fzoss1  13602  fsuppmapnn0fiubex  13915  swrd00  14568  swrdlend  14577  repswswrd  14707  xptrrel  14903  relexpdmd  14967  relexprnd  14971  relexpfldd  14973  rtrclreclem4  14984  sum0  15644  fsumss  15648  fsumcvg3  15652  prod0  15866  0bits  16366  sadid1  16395  sadid2  16396  smu01lem  16412  smu01  16413  smu02  16414  lcmf0  16561  vdwmc2  16907  vdwlem13  16921  ramz2  16952  strfvss  17114  ressbasssg  17164  ressbasssOLD  17167  ress0  17170  ismred2  17522  acsfn  17582  acsfn0  17583  0ssc  17761  fullfunc  17832  fthfunc  17833  mrelatglb0  18484  cntzssv  19257  symgsssg  19396  efgsfo  19668  dprdsn  19967  lsp0  20960  lss0v  20968  lspsnat  21100  lsppratlem3  21104  lbsexg  21119  evpmss  21541  ocv0  21632  ocvz  21633  css1  21645  resspsrbas  21929  mhp0cl  22089  psr1crng  22127  psr1assa  22128  psr1tos  22129  psr1bas2  22130  vr1cl2  22133  ply1lss  22137  ply1subrg  22138  psr1plusg  22161  psr1vsca  22162  psr1mulr  22163  psr1ring  22187  psr1lmod  22189  psr1sca  22190  0opn  22848  toponsspwpw  22866  basdif0  22897  baspartn  22898  0cld  22982  ntr0  23025  cmpfi  23352  refun0  23459  xkouni  23543  xkoccn  23563  alexsubALTlem2  23992  ptcmplem2  23997  tsmsfbas  24072  setsmstopn  24422  restmetu  24514  tngtopn  24594  iccntr  24766  xrge0gsumle  24778  xrge0tsms  24779  metdstri  24796  ovol0  25450  0mbl  25496  itg1le  25670  itgioo  25773  limcnlp  25835  dvbsss  25859  plyssc  26161  fsumharmonic  26978  nulslts  27771  nulsgts  27772  bday0b  27809  madess  27862  oldssmade  27863  oldss  27866  precsexlem8  28210  bdaypw2n0bndlem  28459  bdaypw2n0bnd  28460  egrsubgr  29350  0grsubgr  29351  0uhgrsubgr  29352  chocnul  31403  span0  31617  chsup0  31623  ssnnssfz  32867  indconst0  32939  xrge0tsmsd  33155  elrgspnlem4  33327  unitprodclb  33470  constrfiss  33908  ddemeas  34393  dya2iocuni  34440  oms0  34454  0elcarsg  34464  eulerpartlemt  34528  bnj1143  34946  mrsubrn  35707  msubrn  35723  mthmpps  35776  bj-nuliotaALT  37259  bj-restsn0  37290  bj-restsn10  37291  bj-imdirco  37395  pibt2  37622  mblfinlem2  37859  mblfinlem3  37860  ismblfin  37862  sstotbnd2  37975  isbnd3  37985  ssbnd  37989  heiborlem6  38017  lub0N  39449  glb0N  39453  0psubN  40009  padd01  40071  padd02  40072  pol0N  40169  pcl0N  40182  0psubclN  40203  mzpcompact2lem  42993  itgocn  43406  oaabsb  43536  oege1  43548  nnoeomeqom  43554  cantnfresb  43566  omabs2  43574  omcl2  43575  tfsconcatb0  43586  nadd2rabex  43628  fpwfvss  43653  nla0002  43665  nla0003  43666  nla0001  43667  fvnonrel  43838  clcnvlem  43864  cnvrcl0  43866  cnvtrcl0  43867  0he  44023  ntrclskb  44310  gru0eld  44470  mnu0eld  44506  mnuprdlem4  44516  mnuprd  44517  founiiun0  45434  uzfissfz  45571  limcdm0  45864  cncfiooicc  46138  itgvol0  46212  ibliooicc  46215  ovn0  46810  sprssspr  47727  isubgr0uhgr  48119  ssnn0ssfz  48595  ipolub0  49237  ipoglb0  49239  discsubc  49309  iinfconstbas  49311  nelsubclem  49312  setc1onsubc  49847  setrec2fun  49937  setrec2mpt  49942