Theorem 0ss 4395

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

Syntax hints:   ∈ wcel 2107   ⊆ wss 3947  ∅c0 4321

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3950  df-in 3954  df-ss 3964  df-nul 4322

This theorem is referenced by:  ss0b  4396  0pss  4443  npss0  4444  ssdifeq0  4485  pwpw0  4815  sssn  4828  sspr  4835  sstp  4836  pwsnOLD  4900  uni0  4938  int0el  4982  0disj  5139  disjx0  5141  tr0  5277  al0ssb  5307  0elpw  5353  rel0  5797  0ima  6074  dmxpss  6167  dmsnopss  6210  dfpo2  6292  on0eqel  6485  iotassuni  6512  iotassuniOLD  6519  fun0  6610  f0  6769  fvmptss  7006  fvmptss2  7019  funressn  7152  riotassuni  7401  ordsuci  7791  frxp  8107  suppssdm  8157  suppun  8164  suppss  8174  suppssOLD  8175  suppssov1  8178  suppss2  8180  suppssfv  8182  oaword1  8548  oaword2  8549  omwordri  8568  oewordri  8588  oeworde  8589  nnaword1  8625  naddword1  8686  mapssfset  8841  0domgOLD  9097  fodomr  9124  pwdom  9125  php  9206  phpOLD  9218  isinf  9256  isinfOLD  9257  finsschain  9355  fipwuni  9417  fipwss  9420  wdompwdom  9569  inf3lemd  9618  inf3lem1  9619  cantnfle  9662  ttrclselem1  9716  tc0  9738  r1val1  9777  alephgeom  10073  infmap2  10209  cfub  10240  cf0  10242  cflecard  10244  cfle  10245  fin23lem16  10326  itunitc1  10411  ttukeylem6  10505  ttukeylem7  10506  canthwe  10642  wun0  10709  tsk0  10754  gruina  10809  grur1a  10810  uzssz  12839  xrsup0  13298  fzoss1  13655  fsuppmapnn0fiubex  13953  swrd00  14590  swrdlend  14599  repswswrd  14730  xptrrel  14923  relexpdmd  14987  relexprnd  14991  relexpfldd  14993  rtrclreclem4  15004  sum0  15663  fsumss  15667  fsumcvg3  15671  prod0  15883  0bits  16376  sadid1  16405  sadid2  16406  smu01lem  16422  smu01  16423  smu02  16424  lcmf0  16567  vdwmc2  16908  vdwlem13  16922  ramz2  16953  strfvss  17116  ressbasssg  17177  ressbasssOLD  17180  ress0  17184  ismred2  17543  acsfn  17599  acsfn0  17600  0ssc  17783  fullfunc  17853  fthfunc  17854  mrelatglb0  18510  cntzssv  19186  symgsssg  19328  efgsfo  19600  dprdsn  19898  lsp0  20608  lss0v  20615  lspsnat  20746  lsppratlem3  20750  lbsexg  20765  evpmss  21123  ocv0  21214  ocvz  21215  css1  21227  resspsrbas  21517  mhp0cl  21671  psr1crng  21693  psr1assa  21694  psr1tos  21695  psr1bas2  21696  vr1cl2  21699  ply1lss  21702  ply1subrg  21703  psr1plusg  21726  psr1vsca  21727  psr1mulr  21728  psr1ring  21751  psr1lmod  21753  psr1sca  21754  0opn  22388  toponsspwpw  22406  basdif0  22438  baspartn  22439  0cld  22524  ntr0  22567  cmpfi  22894  refun0  23001  xkouni  23085  xkoccn  23105  alexsubALTlem2  23534  ptcmplem2  23539  tsmsfbas  23614  setsmstopn  23968  restmetu  24061  tngtopn  24149  iccntr  24319  xrge0gsumle  24331  xrge0tsms  24332  metdstri  24349  ovol0  24992  0mbl  25038  itg1le  25213  itgioo  25315  limcnlp  25377  dvbsss  25401  plyssc  25696  fsumharmonic  26496  nulsslt  27278  nulssgt  27279  bday0b  27311  madess  27351  oldssmade  27352  precsexlem8  27640  egrsubgr  28514  0grsubgr  28515  0uhgrsubgr  28516  chocnul  30559  span0  30773  chsup0  30779  ssnnssfz  31976  xrge0tsmsd  32187  ddemeas  33172  dya2iocuni  33220  oms0  33234  0elcarsg  33244  eulerpartlemt  33308  bnj1143  33739  mrsubrn  34442  msubrn  34458  mthmpps  34511  bj-nuliotaALT  35877  bj-restsn0  35904  bj-restsn10  35905  bj-imdirco  36009  pibt2  36236  mblfinlem2  36464  mblfinlem3  36465  ismblfin  36467  sstotbnd2  36580  isbnd3  36590  ssbnd  36594  heiborlem6  36622  lub0N  37997  glb0N  38001  0psubN  38558  padd01  38620  padd02  38621  pol0N  38718  pcl0N  38731  0psubclN  38752  mzpcompact2lem  41422  itgocn  41839  oaabsb  41977  oege1  41989  nnoeomeqom  41995  cantnfresb  42007  omabs2  42015  omcl2  42016  tfsconcatb0  42027  nadd2rabex  42069  fpwfvss  42096  nla0002  42108  nla0003  42109  nla0001  42110  fvnonrel  42281  clcnvlem  42307  cnvrcl0  42309  cnvtrcl0  42310  0he  42466  ntrclskb  42753  gru0eld  42921  mnu0eld  42957  mnuprdlem4  42967  mnuprd  42968  founiiun0  43821  uzfissfz  43971  limcdm0  44269  cncfiooicc  44545  itgvol0  44619  ibliooicc  44622  ovn0  45217  sprssspr  46084  ssnn0ssfz  46927  ipolub0  47519  ipoglb0  47521  setrec2fun  47639  setrec2mpt  47644