Theorem 0ss 4351

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

Syntax hints:   ∈ wcel 2109   ⊆ wss 3903  ∅c0 4284

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-dif 3906  df-ss 3920  df-nul 4285

This theorem is referenced by:  ss0b  4352  0pss  4398  npss0  4399  ssdifeq0  4438  pwpw0  4764  sssn  4777  sspr  4786  sstp  4787  uni0  4886  int0el  4929  0disj  5085  disjx0  5087  tr0  5211  al0ssb  5247  0elpw  5295  rel0  5742  0ima  6029  dmxpss  6120  dmsnopss  6163  dfpo2  6244  on0eqel  6432  iotassuni  6457  fun0  6547  f0  6705  fvmptss  6942  fvmptss2  6956  funressn  7093  riotassuni  7346  ordsuci  7744  frxp  8059  suppssdm  8110  suppun  8117  suppss  8127  suppssov1  8130  suppssov2  8131  suppss2  8133  suppssfv  8135  oaword1  8470  oaword2  8471  omwordri  8490  oewordri  8510  oeworde  8511  nnaword1  8547  naddword1  8609  mapssfset  8778  fodomr  9045  pwdom  9046  php  9121  isinf  9154  fodomfir  9218  finsschain  9249  fipwuni  9316  fipwss  9319  wdompwdom  9470  inf3lemd  9523  inf3lem1  9524  cantnfle  9567  ttrclselem1  9621  tc0  9643  r1val1  9682  alephgeom  9976  infmap2  10111  cfub  10143  cf0  10145  cflecard  10147  cfle  10148  fin23lem16  10229  itunitc1  10314  ttukeylem6  10408  ttukeylem7  10409  canthwe  10545  wun0  10612  tsk0  10657  gruina  10712  grur1a  10713  uzssz  12756  xrsup0  13225  fzoss1  13589  fsuppmapnn0fiubex  13899  swrd00  14551  swrdlend  14560  repswswrd  14690  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  19207  symgsssg  19346  efgsfo  19618  dprdsn  19917  lsp0  20912  lss0v  20920  lspsnat  21052  lsppratlem3  21056  lbsexg  21071  evpmss  21493  ocv0  21584  ocvz  21585  css1  21597  resspsrbas  21881  mhp0cl  22031  psr1crng  22069  psr1assa  22070  psr1tos  22071  psr1bas2  22072  vr1cl2  22075  ply1lss  22079  ply1subrg  22080  psr1plusg  22103  psr1vsca  22104  psr1mulr  22105  psr1ring  22129  psr1lmod  22131  psr1sca  22132  0opn  22789  toponsspwpw  22807  basdif0  22838  baspartn  22839  0cld  22923  ntr0  22966  cmpfi  23293  refun0  23400  xkouni  23484  xkoccn  23504  alexsubALTlem2  23933  ptcmplem2  23938  tsmsfbas  24013  setsmstopn  24364  restmetu  24456  tngtopn  24536  iccntr  24708  xrge0gsumle  24720  xrge0tsms  24721  metdstri  24738  ovol0  25392  0mbl  25438  itg1le  25612  itgioo  25715  limcnlp  25777  dvbsss  25801  plyssc  26103  fsumharmonic  26920  nulsslt  27709  nulssgt  27710  bday0b  27745  madess  27792  oldssmade  27793  oldss  27794  precsexlem8  28123  egrsubgr  29226  0grsubgr  29227  0uhgrsubgr  29228  chocnul  31276  span0  31490  chsup0  31496  ssnnssfz  32739  xrge0tsmsd  33024  elrgspnlem4  33194  unitprodclb  33335  constrfiss  33734  ddemeas  34219  dya2iocuni  34267  oms0  34281  0elcarsg  34291  eulerpartlemt  34355  bnj1143  34773  mrsubrn  35506  msubrn  35522  mthmpps  35575  bj-nuliotaALT  37052  bj-restsn0  37079  bj-restsn10  37080  bj-imdirco  37184  pibt2  37411  mblfinlem2  37658  mblfinlem3  37659  ismblfin  37661  sstotbnd2  37774  isbnd3  37784  ssbnd  37788  heiborlem6  37816  lub0N  39188  glb0N  39192  0psubN  39748  padd01  39810  padd02  39811  pol0N  39908  pcl0N  39921  0psubclN  39942  mzpcompact2lem  42744  itgocn  43157  oaabsb  43287  oege1  43299  nnoeomeqom  43305  cantnfresb  43317  omabs2  43325  omcl2  43326  tfsconcatb0  43337  nadd2rabex  43379  fpwfvss  43405  nla0002  43417  nla0003  43418  nla0001  43419  fvnonrel  43590  clcnvlem  43616  cnvrcl0  43618  cnvtrcl0  43619  0he  43775  ntrclskb  44062  gru0eld  44222  mnu0eld  44258  mnuprdlem4  44268  mnuprd  44269  founiiun0  45188  uzfissfz  45326  limcdm0  45619  cncfiooicc  45895  itgvol0  45969  ibliooicc  45972  ovn0  46567  sprssspr  47485  isubgr0uhgr  47877  ssnn0ssfz  48353  ipolub0  48996  ipoglb0  48998  discsubc  49069  iinfconstbas  49071  nelsubclem  49072  setc1onsubc  49607  setrec2fun  49697  setrec2mpt  49702