Theorem 0ss 4380

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

Syntax hints:   ∈ wcel 2109   ⊆ wss 3931  ∅c0 4313

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-dif 3934  df-ss 3948  df-nul 4314

This theorem is referenced by:  ss0b  4381  0pss  4427  npss0  4428  ssdifeq0  4467  pwpw0  4794  sssn  4807  sspr  4816  sstp  4817  uni0  4916  int0el  4960  0disj  5117  disjx0  5119  tr0  5247  al0ssb  5283  0elpw  5331  rel0  5783  0ima  6070  dmxpss  6165  dmsnopss  6208  dfpo2  6290  on0eqel  6483  iotassuni  6508  iotassuniOLD  6515  fun0  6606  f0  6764  fvmptss  7003  fvmptss2  7017  funressn  7154  riotassuni  7407  ordsuci  7807  frxp  8130  suppssdm  8181  suppun  8188  suppss  8198  suppssov1  8201  suppssov2  8202  suppss2  8204  suppssfv  8206  oaword1  8569  oaword2  8570  omwordri  8589  oewordri  8609  oeworde  8610  nnaword1  8646  naddword1  8708  mapssfset  8870  0domgOLD  9120  fodomr  9147  pwdom  9148  php  9226  phpOLD  9236  isinf  9273  isinfOLD  9274  fodomfir  9345  finsschain  9376  fipwuni  9443  fipwss  9446  wdompwdom  9597  inf3lemd  9646  inf3lem1  9647  cantnfle  9690  ttrclselem1  9744  tc0  9766  r1val1  9805  alephgeom  10101  infmap2  10236  cfub  10268  cf0  10270  cflecard  10272  cfle  10273  fin23lem16  10354  itunitc1  10439  ttukeylem6  10533  ttukeylem7  10534  canthwe  10670  wun0  10737  tsk0  10782  gruina  10837  grur1a  10838  uzssz  12878  xrsup0  13344  fzoss1  13708  fsuppmapnn0fiubex  14015  swrd00  14667  swrdlend  14676  repswswrd  14807  xptrrel  15004  relexpdmd  15068  relexprnd  15072  relexpfldd  15074  rtrclreclem4  15085  sum0  15742  fsumss  15746  fsumcvg3  15750  prod0  15964  0bits  16463  sadid1  16492  sadid2  16493  smu01lem  16509  smu01  16510  smu02  16511  lcmf0  16658  vdwmc2  17004  vdwlem13  17018  ramz2  17049  strfvss  17211  ressbasssg  17263  ressbasssOLD  17266  ress0  17269  ismred2  17620  acsfn  17676  acsfn0  17677  0ssc  17855  fullfunc  17926  fthfunc  17927  mrelatglb0  18576  cntzssv  19316  symgsssg  19453  efgsfo  19725  dprdsn  20024  lsp0  20971  lss0v  20979  lspsnat  21111  lsppratlem3  21115  lbsexg  21130  evpmss  21551  ocv0  21642  ocvz  21643  css1  21655  resspsrbas  21939  mhp0cl  22089  psr1crng  22127  psr1assa  22128  psr1tos  22129  psr1bas2  22130  vr1cl2  22133  ply1lss  22137  ply1subrg  22138  psr1plusg  22161  psr1vsca  22162  psr1mulr  22163  psr1ring  22187  psr1lmod  22189  psr1sca  22190  0opn  22847  toponsspwpw  22865  basdif0  22896  baspartn  22897  0cld  22981  ntr0  23024  cmpfi  23351  refun0  23458  xkouni  23542  xkoccn  23562  alexsubALTlem2  23991  ptcmplem2  23996  tsmsfbas  24071  setsmstopn  24422  restmetu  24514  tngtopn  24594  iccntr  24766  xrge0gsumle  24778  xrge0tsms  24779  metdstri  24796  ovol0  25451  0mbl  25497  itg1le  25671  itgioo  25774  limcnlp  25836  dvbsss  25860  plyssc  26162  fsumharmonic  26979  nulsslt  27766  nulssgt  27767  bday0b  27799  madess  27845  oldssmade  27846  precsexlem8  28173  egrsubgr  29261  0grsubgr  29262  0uhgrsubgr  29263  chocnul  31314  span0  31528  chsup0  31534  ssnnssfz  32769  xrge0tsmsd  33061  elrgspnlem4  33245  unitprodclb  33409  constrfiss  33790  ddemeas  34272  dya2iocuni  34320  oms0  34334  0elcarsg  34344  eulerpartlemt  34408  bnj1143  34826  mrsubrn  35540  msubrn  35556  mthmpps  35609  bj-nuliotaALT  37081  bj-restsn0  37108  bj-restsn10  37109  bj-imdirco  37213  pibt2  37440  mblfinlem2  37687  mblfinlem3  37688  ismblfin  37690  sstotbnd2  37803  isbnd3  37813  ssbnd  37817  heiborlem6  37845  lub0N  39212  glb0N  39216  0psubN  39773  padd01  39835  padd02  39836  pol0N  39933  pcl0N  39946  0psubclN  39967  mzpcompact2lem  42749  itgocn  43163  oaabsb  43293  oege1  43305  nnoeomeqom  43311  cantnfresb  43323  omabs2  43331  omcl2  43332  tfsconcatb0  43343  nadd2rabex  43385  fpwfvss  43411  nla0002  43423  nla0003  43424  nla0001  43425  fvnonrel  43596  clcnvlem  43622  cnvrcl0  43624  cnvtrcl0  43625  0he  43781  ntrclskb  44068  gru0eld  44228  mnu0eld  44264  mnuprdlem4  44274  mnuprd  44275  founiiun0  45194  uzfissfz  45333  limcdm0  45627  cncfiooicc  45903  itgvol0  45977  ibliooicc  45980  ovn0  46575  sprssspr  47475  isubgr0uhgr  47866  ssnn0ssfz  48304  ipolub0  48946  ipoglb0  48948  discsubc  49011  iinfconstbas  49013  nelsubclem  49014  setc1onsubc  49459  setrec2fun  49536  setrec2mpt  49541