Theorem 0ss 4341

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

Syntax hints:   ∈ wcel 2114   ⊆ wss 3890  ∅c0 4274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-dif 3893  df-ss 3907  df-nul 4275

This theorem is referenced by:  ss0b  4342  0pss  4388  npss0  4389  ssdifeq0  4427  pwpw0  4757  sssn  4770  sspr  4779  sstp  4780  uni0OLD  4880  int0el  4922  0disj  5079  disjx0  5081  tr0  5205  al0ssb  5243  0elpw  5293  rel0  5748  0ima  6037  dmxpss  6129  dmsnopss  6172  dfpo2  6254  on0eqel  6442  iotassuni  6467  fun0  6557  f0  6715  fvmptss  6954  fvmptss2  6968  funressn  7106  riotassuni  7357  ordsuci  7755  frxp  8069  suppssdm  8120  suppun  8127  suppss  8137  suppssov1  8140  suppssov2  8141  suppss2  8143  suppssfv  8145  oaword1  8480  oaword2  8481  omwordri  8500  oewordri  8521  oeworde  8522  nnaword1  8558  naddword1  8620  mapssfset  8791  fodomr  9059  pwdom  9060  php  9134  isinf  9168  fodomfir  9231  finsschain  9262  fipwuni  9332  fipwss  9335  wdompwdom  9486  inf3lemd  9539  inf3lem1  9540  cantnfle  9583  ttrclselem1  9637  tc0  9657  r1val1  9701  alephgeom  9995  infmap2  10130  cfub  10162  cf0  10164  cflecard  10166  cfle  10167  fin23lem16  10248  itunitc1  10333  ttukeylem6  10427  ttukeylem7  10428  canthwe  10565  wun0  10632  tsk0  10677  gruina  10732  grur1a  10733  indconst0  12162  uzssz  12800  xrsup0  13266  fzoss1  13632  fsuppmapnn0fiubex  13945  swrd00  14598  swrdlend  14607  repswswrd  14737  xptrrel  14933  relexpdmd  14997  relexprnd  15001  relexpfldd  15003  rtrclreclem4  15014  sum0  15674  fsumss  15678  fsumcvg3  15682  prod0  15899  0bits  16399  sadid1  16428  sadid2  16429  smu01lem  16445  smu01  16446  smu02  16447  lcmf0  16594  vdwmc2  16941  vdwlem13  16955  ramz2  16986  strfvss  17148  ressbasssg  17198  ressbasssOLD  17201  ress0  17204  ismred2  17556  acsfn  17616  acsfn0  17617  0ssc  17795  fullfunc  17866  fthfunc  17867  mrelatglb0  18518  cntzssv  19294  symgsssg  19433  efgsfo  19705  dprdsn  20004  lsp0  20995  lss0v  21003  lspsnat  21135  lsppratlem3  21139  lbsexg  21154  evpmss  21576  ocv0  21667  ocvz  21668  css1  21680  resspsrbas  21962  mhp0cl  22122  psr1crng  22160  psr1assa  22161  psr1tos  22162  psr1bas2  22163  vr1cl2  22166  ply1lss  22170  ply1subrg  22171  psr1plusg  22194  psr1vsca  22195  psr1mulr  22196  psr1ring  22220  psr1lmod  22222  psr1sca  22223  0opn  22879  toponsspwpw  22897  basdif0  22928  baspartn  22929  0cld  23013  ntr0  23056  cmpfi  23383  refun0  23490  xkouni  23574  xkoccn  23594  alexsubALTlem2  24023  ptcmplem2  24028  tsmsfbas  24103  setsmstopn  24453  restmetu  24545  tngtopn  24625  iccntr  24797  xrge0gsumle  24809  xrge0tsms  24810  metdstri  24827  ovol0  25470  0mbl  25516  itg1le  25690  itgioo  25793  limcnlp  25855  dvbsss  25879  plyssc  26175  fsumharmonic  26989  nulslts  27781  nulsgts  27782  bday0b  27819  madess  27872  oldssmade  27873  oldss  27876  precsexlem8  28220  bdaypw2n0bndlem  28469  bdaypw2n0bnd  28470  egrsubgr  29360  0grsubgr  29361  0uhgrsubgr  29362  chocnul  31414  span0  31628  chsup0  31634  ssnnssfz  32875  xrge0tsmsd  33149  elrgspnlem4  33321  unitprodclb  33464  constrfiss  33911  ddemeas  34396  dya2iocuni  34443  oms0  34457  0elcarsg  34467  eulerpartlemt  34531  bnj1143  34948  mrsubrn  35711  msubrn  35727  mthmpps  35780  bj-nuliotaALT  37381  bj-restsn0  37413  bj-restsn10  37414  bj-imdirco  37520  pibt2  37747  mblfinlem2  37993  mblfinlem3  37994  ismblfin  37996  sstotbnd2  38109  isbnd3  38119  ssbnd  38123  heiborlem6  38151  lub0N  39649  glb0N  39653  0psubN  40209  padd01  40271  padd02  40272  pol0N  40369  pcl0N  40382  0psubclN  40403  mzpcompact2lem  43197  itgocn  43610  oaabsb  43740  oege1  43752  nnoeomeqom  43758  cantnfresb  43770  omabs2  43778  omcl2  43779  tfsconcatb0  43790  nadd2rabex  43832  fpwfvss  43857  nla0002  43869  nla0003  43870  nla0001  43871  fvnonrel  44042  clcnvlem  44068  cnvrcl0  44070  cnvtrcl0  44071  0he  44227  ntrclskb  44514  gru0eld  44674  mnu0eld  44710  mnuprdlem4  44720  mnuprd  44721  founiiun0  45638  uzfissfz  45774  limcdm0  46066  cncfiooicc  46340  itgvol0  46414  ibliooicc  46417  ovn0  47012  sprssspr  47953  isubgr0uhgr  48361  ssnn0ssfz  48837  ipolub0  49479  ipoglb0  49481  discsubc  49551  iinfconstbas  49553  nelsubclem  49554  setc1onsubc  50089  setrec2fun  50179  setrec2mpt  50184