Theorem 0ss 4406

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

Syntax hints:   ∈ wcel 2106   ⊆ wss 3963  ∅c0 4339

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-dif 3966  df-ss 3980  df-nul 4340

This theorem is referenced by:  ss0b  4407  0pss  4453  npss0  4454  ssdifeq0  4493  pwpw0  4818  sssn  4831  sspr  4840  sstp  4841  uni0  4940  int0el  4984  0disj  5141  disjx0  5143  tr0  5278  al0ssb  5314  0elpw  5362  rel0  5812  0ima  6098  dmxpss  6193  dmsnopss  6236  dfpo2  6318  on0eqel  6510  iotassuni  6535  iotassuniOLD  6542  fun0  6633  f0  6790  fvmptss  7028  fvmptss2  7042  funressn  7179  riotassuni  7428  ordsuci  7828  frxp  8150  suppssdm  8201  suppun  8208  suppss  8218  suppssov1  8221  suppssov2  8222  suppss2  8224  suppssfv  8226  oaword1  8589  oaword2  8590  omwordri  8609  oewordri  8629  oeworde  8630  nnaword1  8666  naddword1  8728  mapssfset  8890  0domgOLD  9140  fodomr  9167  pwdom  9168  php  9245  phpOLD  9257  isinf  9294  isinfOLD  9295  fodomfir  9366  finsschain  9397  fipwuni  9464  fipwss  9467  wdompwdom  9616  inf3lemd  9665  inf3lem1  9666  cantnfle  9709  ttrclselem1  9763  tc0  9785  r1val1  9824  alephgeom  10120  infmap2  10255  cfub  10287  cf0  10289  cflecard  10291  cfle  10292  fin23lem16  10373  itunitc1  10458  ttukeylem6  10552  ttukeylem7  10553  canthwe  10689  wun0  10756  tsk0  10801  gruina  10856  grur1a  10857  uzssz  12897  xrsup0  13362  fzoss1  13723  fsuppmapnn0fiubex  14030  swrd00  14679  swrdlend  14688  repswswrd  14819  xptrrel  15016  relexpdmd  15080  relexprnd  15084  relexpfldd  15086  rtrclreclem4  15097  sum0  15754  fsumss  15758  fsumcvg3  15762  prod0  15976  0bits  16473  sadid1  16502  sadid2  16503  smu01lem  16519  smu01  16520  smu02  16521  lcmf0  16668  vdwmc2  17013  vdwlem13  17027  ramz2  17058  strfvss  17221  ressbasssg  17282  ressbasssOLD  17285  ress0  17289  ismred2  17648  acsfn  17704  acsfn0  17705  0ssc  17888  fullfunc  17960  fthfunc  17961  mrelatglb0  18619  cntzssv  19359  symgsssg  19500  efgsfo  19772  dprdsn  20071  lsp0  21025  lss0v  21033  lspsnat  21165  lsppratlem3  21169  lbsexg  21184  evpmss  21622  ocv0  21713  ocvz  21714  css1  21726  resspsrbas  22012  mhp0cl  22168  psr1crng  22204  psr1assa  22205  psr1tos  22206  psr1bas2  22207  vr1cl2  22210  ply1lss  22214  ply1subrg  22215  psr1plusg  22238  psr1vsca  22239  psr1mulr  22240  psr1ring  22264  psr1lmod  22266  psr1sca  22267  0opn  22926  toponsspwpw  22944  basdif0  22976  baspartn  22977  0cld  23062  ntr0  23105  cmpfi  23432  refun0  23539  xkouni  23623  xkoccn  23643  alexsubALTlem2  24072  ptcmplem2  24077  tsmsfbas  24152  setsmstopn  24506  restmetu  24599  tngtopn  24687  iccntr  24857  xrge0gsumle  24869  xrge0tsms  24870  metdstri  24887  ovol0  25542  0mbl  25588  itg1le  25763  itgioo  25866  limcnlp  25928  dvbsss  25952  plyssc  26254  fsumharmonic  27070  nulsslt  27857  nulssgt  27858  bday0b  27890  madess  27930  oldssmade  27931  precsexlem8  28253  pw2bday  28433  egrsubgr  29309  0grsubgr  29310  0uhgrsubgr  29311  chocnul  31357  span0  31571  chsup0  31577  ssnnssfz  32796  xrge0tsmsd  33048  elrgspnlem4  33235  unitprodclb  33397  ddemeas  34217  dya2iocuni  34265  oms0  34279  0elcarsg  34289  eulerpartlemt  34353  bnj1143  34783  mrsubrn  35498  msubrn  35514  mthmpps  35567  bj-nuliotaALT  37041  bj-restsn0  37068  bj-restsn10  37069  bj-imdirco  37173  pibt2  37400  mblfinlem2  37645  mblfinlem3  37646  ismblfin  37648  sstotbnd2  37761  isbnd3  37771  ssbnd  37775  heiborlem6  37803  lub0N  39171  glb0N  39175  0psubN  39732  padd01  39794  padd02  39795  pol0N  39892  pcl0N  39905  0psubclN  39926  mzpcompact2lem  42739  itgocn  43153  oaabsb  43284  oege1  43296  nnoeomeqom  43302  cantnfresb  43314  omabs2  43322  omcl2  43323  tfsconcatb0  43334  nadd2rabex  43376  fpwfvss  43402  nla0002  43414  nla0003  43415  nla0001  43416  fvnonrel  43587  clcnvlem  43613  cnvrcl0  43615  cnvtrcl0  43616  0he  43772  ntrclskb  44059  gru0eld  44225  mnu0eld  44261  mnuprdlem4  44271  mnuprd  44272  founiiun0  45133  uzfissfz  45276  limcdm0  45574  cncfiooicc  45850  itgvol0  45924  ibliooicc  45927  ovn0  46522  sprssspr  47406  isubgr0uhgr  47797  ssnn0ssfz  48194  ipolub0  48781  ipoglb0  48783  setrec2fun  48923  setrec2mpt  48928