Theorem 0ss 4340

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

Syntax hints:   ∈ wcel 2114   ⊆ wss 3889  ∅c0 4273

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-dif 3892  df-ss 3906  df-nul 4274

This theorem is referenced by:  ss0b  4341  0pss  4387  npss0  4388  ssdifeq0  4426  pwpw0  4756  sssn  4769  sspr  4778  sstp  4779  uni0OLD  4879  int0el  4921  0disj  5078  disjx0  5080  tr0  5205  al0ssb  5243  0elpw  5297  rel0  5755  0ima  6043  dmxpss  6135  dmsnopss  6178  dfpo2  6260  on0eqel  6448  iotassuni  6473  fun0  6563  f0  6721  fvmptss  6960  fvmptss2  6974  funressn  7113  riotassuni  7364  ordsuci  7762  frxp  8076  suppssdm  8127  suppun  8134  suppss  8144  suppssov1  8147  suppssov2  8148  suppss2  8150  suppssfv  8152  oaword1  8487  oaword2  8488  omwordri  8507  oewordri  8528  oeworde  8529  nnaword1  8565  naddword1  8627  mapssfset  8798  fodomr  9066  pwdom  9067  php  9141  isinf  9175  fodomfir  9238  finsschain  9269  fipwuni  9339  fipwss  9342  wdompwdom  9493  inf3lemd  9548  inf3lem1  9549  cantnfle  9592  ttrclselem1  9646  tc0  9666  r1val1  9710  alephgeom  10004  infmap2  10139  cfub  10171  cf0  10173  cflecard  10175  cfle  10176  fin23lem16  10257  itunitc1  10342  ttukeylem6  10436  ttukeylem7  10437  canthwe  10574  wun0  10641  tsk0  10686  gruina  10741  grur1a  10742  indconst0  12171  uzssz  12809  xrsup0  13275  fzoss1  13641  fsuppmapnn0fiubex  13954  swrd00  14607  swrdlend  14616  repswswrd  14746  xptrrel  14942  relexpdmd  15006  relexprnd  15010  relexpfldd  15012  rtrclreclem4  15023  sum0  15683  fsumss  15687  fsumcvg3  15691  prod0  15908  0bits  16408  sadid1  16437  sadid2  16438  smu01lem  16454  smu01  16455  smu02  16456  lcmf0  16603  vdwmc2  16950  vdwlem13  16964  ramz2  16995  strfvss  17157  ressbasssg  17207  ressbasssOLD  17210  ress0  17213  ismred2  17565  acsfn  17625  acsfn0  17626  0ssc  17804  fullfunc  17875  fthfunc  17876  mrelatglb0  18527  cntzssv  19303  symgsssg  19442  efgsfo  19714  dprdsn  20013  lsp0  21004  lss0v  21011  lspsnat  21143  lsppratlem3  21147  lbsexg  21162  evpmss  21566  ocv0  21657  ocvz  21658  css1  21670  resspsrbas  21952  mhp0cl  22112  psr1crng  22150  psr1assa  22151  psr1tos  22152  psr1bas2  22153  vr1cl2  22156  ply1lss  22160  ply1subrg  22161  psr1plusg  22184  psr1vsca  22185  psr1mulr  22186  psr1ring  22210  psr1lmod  22212  psr1sca  22213  0opn  22869  toponsspwpw  22887  basdif0  22918  baspartn  22919  0cld  23003  ntr0  23046  cmpfi  23373  refun0  23480  xkouni  23564  xkoccn  23584  alexsubALTlem2  24013  ptcmplem2  24018  tsmsfbas  24093  setsmstopn  24443  restmetu  24535  tngtopn  24615  iccntr  24787  xrge0gsumle  24799  xrge0tsms  24800  metdstri  24817  ovol0  25460  0mbl  25506  itg1le  25680  itgioo  25783  limcnlp  25845  dvbsss  25869  plyssc  26165  fsumharmonic  26975  nulslts  27767  nulsgts  27768  bday0b  27805  madess  27858  oldssmade  27859  oldss  27862  precsexlem8  28206  bdaypw2n0bndlem  28455  bdaypw2n0bnd  28456  egrsubgr  29346  0grsubgr  29347  0uhgrsubgr  29348  chocnul  31399  span0  31613  chsup0  31619  ssnnssfz  32860  xrge0tsmsd  33134  elrgspnlem4  33306  unitprodclb  33449  constrfiss  33895  ddemeas  34380  dya2iocuni  34427  oms0  34441  0elcarsg  34451  eulerpartlemt  34515  bnj1143  34932  mrsubrn  35695  msubrn  35711  mthmpps  35764  bj-nuliotaALT  37365  bj-restsn0  37397  bj-restsn10  37398  bj-imdirco  37504  pibt2  37733  mblfinlem2  37979  mblfinlem3  37980  ismblfin  37982  sstotbnd2  38095  isbnd3  38105  ssbnd  38109  heiborlem6  38137  lub0N  39635  glb0N  39639  0psubN  40195  padd01  40257  padd02  40258  pol0N  40355  pcl0N  40368  0psubclN  40389  mzpcompact2lem  43183  itgocn  43592  oaabsb  43722  oege1  43734  nnoeomeqom  43740  cantnfresb  43752  omabs2  43760  omcl2  43761  tfsconcatb0  43772  nadd2rabex  43814  fpwfvss  43839  nla0002  43851  nla0003  43852  nla0001  43853  fvnonrel  44024  clcnvlem  44050  cnvrcl0  44052  cnvtrcl0  44053  0he  44209  ntrclskb  44496  gru0eld  44656  mnu0eld  44692  mnuprdlem4  44702  mnuprd  44703  founiiun0  45620  uzfissfz  45756  limcdm0  46048  cncfiooicc  46322  itgvol0  46396  ibliooicc  46399  ovn0  46994  sprssspr  47941  isubgr0uhgr  48349  ssnn0ssfz  48825  ipolub0  49467  ipoglb0  49469  discsubc  49539  iinfconstbas  49541  nelsubclem  49542  setc1onsubc  50077  setrec2fun  50167  setrec2mpt  50172