Theorem 0ss 4350

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

Syntax hints:   ∈ wcel 2111   ⊆ wss 3902  ∅c0 4283

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-dif 3905  df-ss 3919  df-nul 4284

This theorem is referenced by:  ss0b  4351  0pss  4397  npss0  4398  ssdifeq0  4437  pwpw0  4765  sssn  4778  sspr  4787  sstp  4788  uni0  4887  int0el  4929  0disj  5084  disjx0  5086  tr0  5210  al0ssb  5246  0elpw  5294  rel0  5739  0ima  6027  dmxpss  6118  dmsnopss  6161  dfpo2  6243  on0eqel  6431  iotassuni  6456  fun0  6546  f0  6704  fvmptss  6941  fvmptss2  6955  funressn  7092  riotassuni  7343  ordsuci  7741  frxp  8056  suppssdm  8107  suppun  8114  suppss  8124  suppssov1  8127  suppssov2  8128  suppss2  8130  suppssfv  8132  oaword1  8467  oaword2  8468  omwordri  8487  oewordri  8507  oeworde  8508  nnaword1  8544  naddword1  8606  mapssfset  8775  fodomr  9041  pwdom  9042  php  9116  isinf  9149  fodomfir  9212  finsschain  9243  fipwuni  9310  fipwss  9313  wdompwdom  9464  inf3lemd  9517  inf3lem1  9518  cantnfle  9561  ttrclselem1  9615  tc0  9635  r1val1  9679  alephgeom  9973  infmap2  10108  cfub  10140  cf0  10142  cflecard  10144  cfle  10145  fin23lem16  10226  itunitc1  10311  ttukeylem6  10405  ttukeylem7  10406  canthwe  10542  wun0  10609  tsk0  10654  gruina  10709  grur1a  10710  uzssz  12753  xrsup0  13222  fzoss1  13586  fsuppmapnn0fiubex  13899  swrd00  14552  swrdlend  14561  repswswrd  14691  xptrrel  14887  relexpdmd  14951  relexprnd  14955  relexpfldd  14957  rtrclreclem4  14968  sum0  15628  fsumss  15632  fsumcvg3  15636  prod0  15850  0bits  16350  sadid1  16379  sadid2  16380  smu01lem  16396  smu01  16397  smu02  16398  lcmf0  16545  vdwmc2  16891  vdwlem13  16905  ramz2  16936  strfvss  17098  ressbasssg  17148  ressbasssOLD  17151  ress0  17154  ismred2  17505  acsfn  17565  acsfn0  17566  0ssc  17744  fullfunc  17815  fthfunc  17816  mrelatglb0  18467  cntzssv  19241  symgsssg  19380  efgsfo  19652  dprdsn  19951  lsp0  20943  lss0v  20951  lspsnat  21083  lsppratlem3  21087  lbsexg  21102  evpmss  21524  ocv0  21615  ocvz  21616  css1  21628  resspsrbas  21912  mhp0cl  22062  psr1crng  22100  psr1assa  22101  psr1tos  22102  psr1bas2  22103  vr1cl2  22106  ply1lss  22110  ply1subrg  22111  psr1plusg  22134  psr1vsca  22135  psr1mulr  22136  psr1ring  22160  psr1lmod  22162  psr1sca  22163  0opn  22820  toponsspwpw  22838  basdif0  22869  baspartn  22870  0cld  22954  ntr0  22997  cmpfi  23324  refun0  23431  xkouni  23515  xkoccn  23535  alexsubALTlem2  23964  ptcmplem2  23969  tsmsfbas  24044  setsmstopn  24394  restmetu  24486  tngtopn  24566  iccntr  24738  xrge0gsumle  24750  xrge0tsms  24751  metdstri  24768  ovol0  25422  0mbl  25468  itg1le  25642  itgioo  25745  limcnlp  25807  dvbsss  25831  plyssc  26133  fsumharmonic  26950  nulsslt  27739  nulssgt  27740  bday0b  27775  madess  27822  oldssmade  27823  oldss  27824  precsexlem8  28153  egrsubgr  29256  0grsubgr  29257  0uhgrsubgr  29258  chocnul  31306  span0  31520  chsup0  31526  ssnnssfz  32768  xrge0tsmsd  33040  elrgspnlem4  33210  unitprodclb  33352  constrfiss  33762  ddemeas  34247  dya2iocuni  34294  oms0  34308  0elcarsg  34318  eulerpartlemt  34382  bnj1143  34800  mrsubrn  35555  msubrn  35571  mthmpps  35624  bj-nuliotaALT  37098  bj-restsn0  37125  bj-restsn10  37126  bj-imdirco  37230  pibt2  37457  mblfinlem2  37704  mblfinlem3  37705  ismblfin  37707  sstotbnd2  37820  isbnd3  37830  ssbnd  37834  heiborlem6  37862  lub0N  39234  glb0N  39238  0psubN  39794  padd01  39856  padd02  39857  pol0N  39954  pcl0N  39967  0psubclN  39988  mzpcompact2lem  42790  itgocn  43203  oaabsb  43333  oege1  43345  nnoeomeqom  43351  cantnfresb  43363  omabs2  43371  omcl2  43372  tfsconcatb0  43383  nadd2rabex  43425  fpwfvss  43451  nla0002  43463  nla0003  43464  nla0001  43465  fvnonrel  43636  clcnvlem  43662  cnvrcl0  43664  cnvtrcl0  43665  0he  43821  ntrclskb  44108  gru0eld  44268  mnu0eld  44304  mnuprdlem4  44314  mnuprd  44315  founiiun0  45233  uzfissfz  45371  limcdm0  45664  cncfiooicc  45938  itgvol0  46012  ibliooicc  46015  ovn0  46610  sprssspr  47518  isubgr0uhgr  47910  ssnn0ssfz  48386  ipolub0  49029  ipoglb0  49031  discsubc  49102  iinfconstbas  49104  nelsubclem  49105  setc1onsubc  49640  setrec2fun  49730  setrec2mpt  49735