Theorem 0ss 4354

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

Syntax hints:   ∈ wcel 2114   ⊆ wss 3903  ∅c0 4287

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-dif 3906  df-ss 3920  df-nul 4288

This theorem is referenced by:  ss0b  4355  0pss  4401  npss0  4402  ssdifeq0  4441  pwpw0  4771  sssn  4784  sspr  4793  sstp  4794  uni0OLD  4894  int0el  4936  0disj  5093  disjx0  5095  tr0  5219  al0ssb  5255  0elpw  5303  rel0  5756  0ima  6045  dmxpss  6137  dmsnopss  6180  dfpo2  6262  on0eqel  6450  iotassuni  6475  fun0  6565  f0  6723  fvmptss  6962  fvmptss2  6976  funressn  7114  riotassuni  7365  ordsuci  7763  frxp  8078  suppssdm  8129  suppun  8136  suppss  8146  suppssov1  8149  suppssov2  8150  suppss2  8152  suppssfv  8154  oaword1  8489  oaword2  8490  omwordri  8509  oewordri  8530  oeworde  8531  nnaword1  8567  naddword1  8629  mapssfset  8800  fodomr  9068  pwdom  9069  php  9143  isinf  9177  fodomfir  9240  finsschain  9271  fipwuni  9341  fipwss  9344  wdompwdom  9495  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  uzssz  12784  xrsup0  13250  fzoss1  13614  fsuppmapnn0fiubex  13927  swrd00  14580  swrdlend  14589  repswswrd  14719  xptrrel  14915  relexpdmd  14979  relexprnd  14983  relexpfldd  14985  rtrclreclem4  14996  sum0  15656  fsumss  15660  fsumcvg3  15664  prod0  15878  0bits  16378  sadid1  16407  sadid2  16408  smu01lem  16424  smu01  16425  smu02  16426  lcmf0  16573  vdwmc2  16919  vdwlem13  16933  ramz2  16964  strfvss  17126  ressbasssg  17176  ressbasssOLD  17179  ress0  17182  ismred2  17534  acsfn  17594  acsfn0  17595  0ssc  17773  fullfunc  17844  fthfunc  17845  mrelatglb0  18496  cntzssv  19269  symgsssg  19408  efgsfo  19680  dprdsn  19979  lsp0  20972  lss0v  20980  lspsnat  21112  lsppratlem3  21116  lbsexg  21131  evpmss  21553  ocv0  21644  ocvz  21645  css1  21657  resspsrbas  21941  mhp0cl  22101  psr1crng  22139  psr1assa  22140  psr1tos  22141  psr1bas2  22142  vr1cl2  22145  ply1lss  22149  ply1subrg  22150  psr1plusg  22173  psr1vsca  22174  psr1mulr  22175  psr1ring  22199  psr1lmod  22201  psr1sca  22202  0opn  22860  toponsspwpw  22878  basdif0  22909  baspartn  22910  0cld  22994  ntr0  23037  cmpfi  23364  refun0  23471  xkouni  23555  xkoccn  23575  alexsubALTlem2  24004  ptcmplem2  24009  tsmsfbas  24084  setsmstopn  24434  restmetu  24526  tngtopn  24606  iccntr  24778  xrge0gsumle  24790  xrge0tsms  24791  metdstri  24808  ovol0  25462  0mbl  25508  itg1le  25682  itgioo  25785  limcnlp  25847  dvbsss  25871  plyssc  26173  fsumharmonic  26990  nulslts  27783  nulsgts  27784  bday0b  27821  madess  27874  oldssmade  27875  oldss  27878  precsexlem8  28222  bdaypw2n0bndlem  28471  bdaypw2n0bnd  28472  egrsubgr  29362  0grsubgr  29363  0uhgrsubgr  29364  chocnul  31415  span0  31629  chsup0  31635  ssnnssfz  32877  indconst0  32949  xrge0tsmsd  33166  elrgspnlem4  33338  unitprodclb  33481  constrfiss  33928  ddemeas  34413  dya2iocuni  34460  oms0  34474  0elcarsg  34484  eulerpartlemt  34548  bnj1143  34965  mrsubrn  35726  msubrn  35742  mthmpps  35795  bj-nuliotaALT  37303  bj-restsn0  37335  bj-restsn10  37336  bj-imdirco  37442  pibt2  37669  mblfinlem2  37906  mblfinlem3  37907  ismblfin  37909  sstotbnd2  38022  isbnd3  38032  ssbnd  38036  heiborlem6  38064  lub0N  39562  glb0N  39566  0psubN  40122  padd01  40184  padd02  40185  pol0N  40282  pcl0N  40295  0psubclN  40316  mzpcompact2lem  43105  itgocn  43518  oaabsb  43648  oege1  43660  nnoeomeqom  43666  cantnfresb  43678  omabs2  43686  omcl2  43687  tfsconcatb0  43698  nadd2rabex  43740  fpwfvss  43765  nla0002  43777  nla0003  43778  nla0001  43779  fvnonrel  43950  clcnvlem  43976  cnvrcl0  43978  cnvtrcl0  43979  0he  44135  ntrclskb  44422  gru0eld  44582  mnu0eld  44618  mnuprdlem4  44628  mnuprd  44629  founiiun0  45546  uzfissfz  45682  limcdm0  45975  cncfiooicc  46249  itgvol0  46323  ibliooicc  46326  ovn0  46921  sprssspr  47838  isubgr0uhgr  48230  ssnn0ssfz  48706  ipolub0  49348  ipoglb0  49350  discsubc  49420  iinfconstbas  49422  nelsubclem  49423  setc1onsubc  49958  setrec2fun  50048  setrec2mpt  50053