Theorem 0ss 4363

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

Syntax hints:   ∈ wcel 2109   ⊆ wss 3914  ∅c0 4296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-dif 3917  df-ss 3931  df-nul 4297

This theorem is referenced by:  ss0b  4364  0pss  4410  npss0  4411  ssdifeq0  4450  pwpw0  4777  sssn  4790  sspr  4799  sstp  4800  uni0  4899  int0el  4943  0disj  5100  disjx0  5102  tr0  5227  al0ssb  5263  0elpw  5311  rel0  5762  0ima  6049  dmxpss  6144  dmsnopss  6187  dfpo2  6269  on0eqel  6458  iotassuni  6483  iotassuniOLD  6490  fun0  6581  f0  6741  fvmptss  6980  fvmptss2  6994  funressn  7131  riotassuni  7384  ordsuci  7784  frxp  8105  suppssdm  8156  suppun  8163  suppss  8173  suppssov1  8176  suppssov2  8177  suppss2  8179  suppssfv  8181  oaword1  8516  oaword2  8517  omwordri  8536  oewordri  8556  oeworde  8557  nnaword1  8593  naddword1  8655  mapssfset  8824  fodomr  9092  pwdom  9093  php  9171  isinf  9207  isinfOLD  9208  fodomfir  9279  finsschain  9310  fipwuni  9377  fipwss  9380  wdompwdom  9531  inf3lemd  9580  inf3lem1  9581  cantnfle  9624  ttrclselem1  9678  tc0  9700  r1val1  9739  alephgeom  10035  infmap2  10170  cfub  10202  cf0  10204  cflecard  10206  cfle  10207  fin23lem16  10288  itunitc1  10373  ttukeylem6  10467  ttukeylem7  10468  canthwe  10604  wun0  10671  tsk0  10716  gruina  10771  grur1a  10772  uzssz  12814  xrsup0  13283  fzoss1  13647  fsuppmapnn0fiubex  13957  swrd00  14609  swrdlend  14618  repswswrd  14749  xptrrel  14946  relexpdmd  15010  relexprnd  15014  relexpfldd  15016  rtrclreclem4  15027  sum0  15687  fsumss  15691  fsumcvg3  15695  prod0  15909  0bits  16409  sadid1  16438  sadid2  16439  smu01lem  16455  smu01  16456  smu02  16457  lcmf0  16604  vdwmc2  16950  vdwlem13  16964  ramz2  16995  strfvss  17157  ressbasssg  17207  ressbasssOLD  17210  ress0  17213  ismred2  17564  acsfn  17620  acsfn0  17621  0ssc  17799  fullfunc  17870  fthfunc  17871  mrelatglb0  18520  cntzssv  19260  symgsssg  19397  efgsfo  19669  dprdsn  19968  lsp0  20915  lss0v  20923  lspsnat  21055  lsppratlem3  21059  lbsexg  21074  evpmss  21495  ocv0  21586  ocvz  21587  css1  21599  resspsrbas  21883  mhp0cl  22033  psr1crng  22071  psr1assa  22072  psr1tos  22073  psr1bas2  22074  vr1cl2  22077  ply1lss  22081  ply1subrg  22082  psr1plusg  22105  psr1vsca  22106  psr1mulr  22107  psr1ring  22131  psr1lmod  22133  psr1sca  22134  0opn  22791  toponsspwpw  22809  basdif0  22840  baspartn  22841  0cld  22925  ntr0  22968  cmpfi  23295  refun0  23402  xkouni  23486  xkoccn  23506  alexsubALTlem2  23935  ptcmplem2  23940  tsmsfbas  24015  setsmstopn  24366  restmetu  24458  tngtopn  24538  iccntr  24710  xrge0gsumle  24722  xrge0tsms  24723  metdstri  24740  ovol0  25394  0mbl  25440  itg1le  25614  itgioo  25717  limcnlp  25779  dvbsss  25803  plyssc  26105  fsumharmonic  26922  nulsslt  27709  nulssgt  27710  bday0b  27742  madess  27788  oldssmade  27789  precsexlem8  28116  egrsubgr  29204  0grsubgr  29205  0uhgrsubgr  29206  chocnul  31257  span0  31471  chsup0  31477  ssnnssfz  32710  xrge0tsmsd  33002  elrgspnlem4  33196  unitprodclb  33360  constrfiss  33741  ddemeas  34226  dya2iocuni  34274  oms0  34288  0elcarsg  34298  eulerpartlemt  34362  bnj1143  34780  mrsubrn  35500  msubrn  35516  mthmpps  35569  bj-nuliotaALT  37046  bj-restsn0  37073  bj-restsn10  37074  bj-imdirco  37178  pibt2  37405  mblfinlem2  37652  mblfinlem3  37653  ismblfin  37655  sstotbnd2  37768  isbnd3  37778  ssbnd  37782  heiborlem6  37810  lub0N  39182  glb0N  39186  0psubN  39743  padd01  39805  padd02  39806  pol0N  39903  pcl0N  39916  0psubclN  39937  mzpcompact2lem  42739  itgocn  43153  oaabsb  43283  oege1  43295  nnoeomeqom  43301  cantnfresb  43313  omabs2  43321  omcl2  43322  tfsconcatb0  43333  nadd2rabex  43375  fpwfvss  43401  nla0002  43413  nla0003  43414  nla0001  43415  fvnonrel  43586  clcnvlem  43612  cnvrcl0  43614  cnvtrcl0  43615  0he  43771  ntrclskb  44058  gru0eld  44218  mnu0eld  44254  mnuprdlem4  44264  mnuprd  44265  founiiun0  45184  uzfissfz  45322  limcdm0  45616  cncfiooicc  45892  itgvol0  45966  ibliooicc  45969  ovn0  46564  sprssspr  47482  isubgr0uhgr  47873  ssnn0ssfz  48337  ipolub0  48980  ipoglb0  48982  discsubc  49053  iinfconstbas  49055  nelsubclem  49056  setc1onsubc  49591  setrec2fun  49681  setrec2mpt  49686