Theorem 0ss 4353

Description: The empty set is a subset of any class. Dual of ssv 3937. 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 4286	. . 3 ⊢ ¬ 𝑥 ∈ ∅
2	1	pm2.21i 120	. 2 ⊢ (𝑥 ∈ ∅ → 𝑥 ∈ 𝐴)
3	2	ssriv 3917	1 ⊢ ∅ ⊆ 𝐴

This proof depends on syntax axioms:   ∈ wcel 2147   ⊆ wss 3900  ∅c0 4281

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ss 3901  df-dif 4050  df-nul 4282

This theorem is used by:  ss0b  4354  0pss  4363  npss0  4364  ssdifeq0  4445  sssn  4787  sspr  4795  sstp  4796  pwpw0  4836  uni0OLD  4902  int0el  4944  0disj  5101  disjx0  5103  tr0  5231  al0ssb  5268  0elpw  5324  rel0  5785  dmxpss  6181  0ima  6219  dmsnopss  6234  dfpo2  6325  on0eqel  6514  iotassuni  6540  fun0  6635  f0  6793  fvmptss  7037  fvmptss2  7051  funressn  7195  riotassuni  7448  ordsuci  7856  frxp  8175  suppssdm  8232  suppun  8239  suppss  8249  suppssov1  8252  suppssov2  8253  suppss2  8255  suppssfv  8257  oaword1  8598  oaword2  8599  omwordri  8618  oewordri  8639  oeworde  8640  nnaword1  8676  naddword1  8739  mapssfset  8911  fodomr  9185  pwdom  9186  php  9260  isinf  9294  fodomfir  9357  finsschain  9386  fipwuni  9455  fipwss  9458  wdompwdom  9609  inf3lemd  9665  inf3lem1  9666  cantnfle  9709  ttrclselem1  9763  tc0  9783  r1val1  9830  setrec2fun  10010  alephgeom  10200  infmap2  10334  cfub  10365  cf0  10367  cflecard  10369  cfle  10370  fin23lem16  10452  itunitc1  10537  ttukeylem6  10631  ttukeylem7  10632  canthwe  10775  wun0  10842  tsk0  10887  gruina  10942  grur1a  10943  indconst0  12372  uzssz  13026  xrsup0  13493  fzoss1  13861  fsuppmapnn0fiubex  14175  swrd00  14834  swrdlend  14845  repswswrd  14977  xptrrel  15176  relexpdmd  15240  relexprnd  15244  relexpfldd  15246  rtrclreclem4  15257  sum0  15931  fsumss  15935  fsumcvg3  15939  prod0  16154  0bits  16653  sadid1  16682  sadid2  16683  smu01lem  16699  smu01  16700  smu02  16701  lcmf0  16853  vdwmc2  17201  vdwlem13  17215  ramz2  17246  strfvss  17409  ressbasssg  17459  ressbasssOLD  17462  ress0  17465  ismred2  17823  acsfn  17883  acsfn0  17884  0ssc  18062  fullfunc  18133  fthfunc  18134  mrelatglb0  18785  cntzssv  19593  symgsssg  19732  efgsfo  20004  dprdsn  20303  lsp0  21335  lss0v  21342  lspsnat  21474  lsppratlem3  21478  lbsexg  21493  evpmss  21947  ocv0  22038  ocvz  22039  css1  22051  resspsrbas  22336  mhp0cl  22522  psr1crng  22560  psr1assa  22561  psr1tos  22562  psr1bas2  22563  vr1cl2  22566  ply1lss  22569  ply1subrg  22570  psr1plusg  22593  psr1vsca  22594  psr1mulr  22595  psr1ring  22619  psr1lmod  22621  psr1sca  22622  0opn  23277  toponsspwpw  23295  basdif0  23326  baspartn  23327  0cld  23411  ntr0  23454  cmpfi  23781  refun0  23889  xkouni  23973  xkoccn  23993  alexsubALTlem2  24422  ptcmplem2  24427  tsmsfbas  24502  setsmstopn  24852  restmetu  24944  tngtopn  25024  iccntr  25196  xrge0gsumle  25208  xrge0tsms  25209  metdstri  25226  ovol0  25869  0mbl  25915  itg1le  26089  itgioo  26191  limcnlp  26253  dvbsss  26277  plyssc  26573  fsumharmonic  27396  nulslts  28218  nulsgts  28219  bday0b  28256  madess  28309  oldssmade  28310  oldss  28313  precsexlem8  28657  bdaypw2n0bndlem  28906  bdaypw2n0bnd  28907  egrsubgr  29915  0grsubgr  29916  0uhgrsubgr  29917  chocnul  31987  span0  32201  chsup0  32207  ssnnssfz  33475  xrge0tsmsd  33733  elrgspnlem4  33905  unitprodclb  34048  constrfiss  34494  ddemeas  34980  dya2iocuni  35026  oms0  35040  0elcarsg  35050  eulerpartlemt  35114  bnj1143  35531  rankscottu  35880  rankkardu  35980  mrsubrn  36486  msubrn  36502  mthmpps  36555  elpssex  36672  elpssmo  36673  nmulss1  37178  bj-nuliotaALT  38243  bj-restsn0  38276  bj-restsn10  38277  bj-pr0moore  38307  bj-imdirco  38379  pibt2  38608  mblfinlem2  38844  mblfinlem3  38845  ismblfin  38847  varprop  38910  sstotbnd2  38974  isbnd3  38984  ssbnd  38988  heiborlem6  39016  lub0N  40512  glb0N  40516  0psubN  41072  padd01  41134  padd02  41135  pol0N  41232  pcl0N  41245  0psubclN  41266  mzpcompact2lem  44028  itgocn  44431  oaabsb  44557  oege1  44569  nnoeomeqom  44575  cantnfresb  44587  omabs2  44595  omcl2  44596  tfsconcatb0  44607  nadd2rabex  44649  fpwfvss  44674  nla0002  44686  nla0003  44687  nla0001  44688  fvnonrel  44858  clcnvlem  44884  cnvrcl0  44886  cnvtrcl0  44887  0he  45043  ntrclskb  45330  gru0eld  45488  mnu0eld  45510  mnuprdlem4  45520  mnuprd  45521  founiiun0  46478  uzfissfz  46611  limcdm0  46903  cncfiooicc  47177  itgvol0  47251  ibliooicc  47254  ovn0  47849  sprssspr  48836  isubgr0uhgr  49244  ssnn0ssfz  49792  ipolub0  50437  ipoglb0  50439  discsubc  50509  iinfconstbas  50511  nelsubclem  50512  setc1onsubc  51071  setrec2mpt  51196