Theorem 0ss 4350

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

This proof depends on syntax axioms:   ∈ wcel 2145   ⊆ wss 3899  ∅c0 4279

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-dif 3902  df-ss 3916  df-nul 4280

This theorem is used by:  ss0b  4351  0pss  4360  npss0  4361  ssdifeq0  4442  pwpw0  4774  sssn  4787  sspr  4795  sstp  4796  uni0OLD  4897  int0el  4939  0disj  5096  disjx0  5098  tr0  5225  al0ssb  5262  0elpw  5317  rel0  5776  dmxpss  6163  0ima  6199  dmsnopss  6214  dfpo2  6298  on0eqel  6487  iotassuni  6512  fun0  6603  f0  6761  fvmptss  7004  fvmptss2  7018  funressn  7161  riotassuni  7415  ordsuci  7820  frxp  8136  suppssdm  8187  suppun  8194  suppss  8204  suppssov1  8207  suppssov2  8208  suppss2  8210  suppssfv  8212  oaword1  8553  oaword2  8554  omwordri  8573  oewordri  8594  oeworde  8595  nnaword1  8631  naddword1  8694  mapssfset  8866  fodomr  9140  pwdom  9141  php  9215  isinf  9249  fodomfir  9312  finsschain  9341  fipwuni  9411  fipwss  9414  wdompwdom  9565  inf3lemd  9621  inf3lem1  9622  cantnfle  9665  ttrclselem1  9719  tc0  9739  r1val1  9786  setrec2fun  9966  alephgeom  10154  infmap2  10288  cfub  10319  cf0  10321  cflecard  10323  cfle  10324  fin23lem16  10406  itunitc1  10491  ttukeylem6  10585  ttukeylem7  10586  canthwe  10729  wun0  10796  tsk0  10841  gruina  10896  grur1a  10897  indconst0  12325  uzssz  12979  xrsup0  13446  fzoss1  13814  fsuppmapnn0fiubex  14128  swrd00  14785  swrdlend  14796  repswswrd  14928  xptrrel  15126  relexpdmd  15190  relexprnd  15194  relexpfldd  15196  rtrclreclem4  15207  sum0  15880  fsumss  15884  fsumcvg3  15888  prod0  16103  0bits  16602  sadid1  16631  sadid2  16632  smu01lem  16648  smu01  16649  smu02  16650  lcmf0  16802  vdwmc2  17150  vdwlem13  17164  ramz2  17195  strfvss  17358  ressbasssg  17408  ressbasssOLD  17411  ress0  17414  ismred2  17766  acsfn  17826  acsfn0  17827  0ssc  18005  fullfunc  18076  fthfunc  18077  mrelatglb0  18728  cntzssv  19535  symgsssg  19674  efgsfo  19946  dprdsn  20245  lsp0  21277  lss0v  21284  lspsnat  21416  lsppratlem3  21420  lbsexg  21435  evpmss  21885  ocv0  21976  ocvz  21977  css1  21989  resspsrbas  22274  mhp0cl  22460  psr1crng  22498  psr1assa  22499  psr1tos  22500  psr1bas2  22501  vr1cl2  22504  ply1lss  22507  ply1subrg  22508  psr1plusg  22531  psr1vsca  22532  psr1mulr  22533  psr1ring  22557  psr1lmod  22559  psr1sca  22560  0opn  23215  toponsspwpw  23233  basdif0  23264  baspartn  23265  0cld  23349  ntr0  23392  cmpfi  23719  refun0  23827  xkouni  23911  xkoccn  23931  alexsubALTlem2  24360  ptcmplem2  24365  tsmsfbas  24440  setsmstopn  24790  restmetu  24882  tngtopn  24962  iccntr  25134  xrge0gsumle  25146  xrge0tsms  25147  metdstri  25164  ovol0  25807  0mbl  25853  itg1le  26027  itgioo  26129  limcnlp  26191  dvbsss  26215  plyssc  26511  fsumharmonic  27332  nulslts  28154  nulsgts  28155  bday0b  28192  madess  28245  oldssmade  28246  oldss  28249  precsexlem8  28593  bdaypw2n0bndlem  28842  bdaypw2n0bnd  28843  egrsubgr  29851  0grsubgr  29852  0uhgrsubgr  29853  chocnul  31923  span0  32137  chsup0  32143  ssnnssfz  33372  xrge0tsmsd  33627  elrgspnlem4  33799  unitprodclb  33937  constrfiss  34376  ddemeas  34862  dya2iocuni  34908  oms0  34922  0elcarsg  34932  eulerpartlemt  34996  bnj1143  35413  rankscottu  35741  rankkardu  35822  mrsubrn  36257  msubrn  36273  mthmpps  36326  nmulss1  36943  bj-nuliotaALT  37953  bj-restsn0  37986  bj-restsn10  37987  bj-imdirco  38091  pibt2  38320  mblfinlem2  38556  mblfinlem3  38557  ismblfin  38559  varprop  38622  sstotbnd2  38688  isbnd3  38698  ssbnd  38702  heiborlem6  38730  lub0N  40226  glb0N  40230  0psubN  40786  padd01  40848  padd02  40849  pol0N  40946  pcl0N  40959  0psubclN  40980  mzpcompact2lem  43741  itgocn  44150  oaabsb  44280  oege1  44292  nnoeomeqom  44298  cantnfresb  44310  omabs2  44318  omcl2  44319  tfsconcatb0  44330  nadd2rabex  44372  fpwfvss  44397  nla0002  44409  nla0003  44410  nla0001  44411  fvnonrel  44582  clcnvlem  44608  cnvrcl0  44610  cnvtrcl0  44611  0he  44767  ntrclskb  45054  gru0eld  45212  mnu0eld  45234  mnuprdlem4  45244  mnuprd  45245  founiiun0  46174  uzfissfz  46307  limcdm0  46599  cncfiooicc  46873  itgvol0  46947  ibliooicc  46950  ovn0  47545  sprssspr  48532  isubgr0uhgr  48940  ssnn0ssfz  49430  ipolub0  50069  ipoglb0  50071  discsubc  50141  iinfconstbas  50143  nelsubclem  50144  setc1onsubc  50679  setrec2mpt  50759