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

Syntax hints:   ∈ wcel 2141   ⊆ wss 3902  ∅c0 4283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-dif 3905  df-ss 3919  df-nul 4284

This theorem is referenced by:  ss0b  4352  0pss  4398  npss0  4399  ssdifeq0  4437  pwpw0  4768  sssn  4781  sspr  4790  sstp  4791  uni0OLD  4892  int0el  4934  0disj  5090  disjx0  5092  tr0  5217  al0ssb  5255  0elpw  5309  rel0  5767  0ima  6062  dmxpss  6151  dmsnopss  6195  dfpo2  6277  on0eqel  6465  iotassuni  6490  fun0  6580  f0  6739  fvmptss  6982  fvmptss2  6996  funressn  7136  riotassuni  7387  ordsuci  7785  frxp  8099  suppssdm  8150  suppun  8157  suppss  8167  suppssov1  8170  suppssov2  8171  suppss2  8173  suppssfv  8175  oaword1  8514  oaword2  8515  omwordri  8534  oewordri  8555  oeworde  8556  nnaword1  8592  naddword1  8655  mapssfset  8825  fodomr  9093  pwdom  9094  php  9168  isinf  9202  fodomfir  9265  finsschain  9295  fipwuni  9365  fipwss  9368  wdompwdom  9519  inf3lemd  9575  inf3lem1  9576  cantnfle  9619  ttrclselem1  9673  tc0  9693  r1val1  9737  alephgeom  10031  infmap2  10166  cfub  10198  cf0  10200  cflecard  10202  cfle  10203  fin23lem16  10285  itunitc1  10370  ttukeylem6  10464  ttukeylem7  10465  canthwe  10602  wun0  10669  tsk0  10714  gruina  10769  grur1a  10770  indconst0  12200  uzssz  12853  xrsup0  13319  fzoss1  13685  fsuppmapnn0fiubex  13998  swrd00  14651  swrdlend  14660  repswswrd  14790  xptrrel  14986  relexpdmd  15050  relexprnd  15054  relexpfldd  15056  rtrclreclem4  15067  sum0  15738  fsumss  15742  fsumcvg3  15746  prod0  15963  0bits  16463  sadid1  16492  sadid2  16493  smu01lem  16509  smu01  16510  smu02  16511  lcmf0  16658  vdwmc2  17005  vdwlem13  17019  ramz2  17050  strfvss  17213  ressbasssg  17263  ressbasssOLD  17266  ress0  17269  ismred2  17621  acsfn  17681  acsfn0  17682  0ssc  17860  fullfunc  17931  fthfunc  17932  mrelatglb0  18583  cntzssv  19358  symgsssg  19497  efgsfo  19769  dprdsn  20068  lsp0  21063  lss0v  21070  lspsnat  21202  lsppratlem3  21206  lbsexg  21221  evpmss  21625  ocv0  21716  ocvz  21717  css1  21729  resspsrbas  22012  mhp0cl  22198  psr1crng  22236  psr1assa  22237  psr1tos  22238  psr1bas2  22239  vr1cl2  22242  ply1lss  22245  ply1subrg  22246  psr1plusg  22269  psr1vsca  22270  psr1mulr  22271  psr1ring  22295  psr1lmod  22297  psr1sca  22298  0opn  22951  toponsspwpw  22969  basdif0  23000  baspartn  23001  0cld  23085  ntr0  23128  cmpfi  23455  refun0  23562  xkouni  23646  xkoccn  23666  alexsubALTlem2  24095  ptcmplem2  24100  tsmsfbas  24175  setsmstopn  24525  restmetu  24617  tngtopn  24697  iccntr  24869  xrge0gsumle  24881  xrge0tsms  24882  metdstri  24899  ovol0  25542  0mbl  25588  itg1le  25762  itgioo  25865  limcnlp  25927  dvbsss  25951  plyssc  26247  fsumharmonic  27063  nulslts  27855  nulsgts  27856  bday0b  27893  madess  27946  oldssmade  27947  oldss  27950  precsexlem8  28294  bdaypw2n0bndlem  28543  bdaypw2n0bnd  28544  egrsubgr  29434  0grsubgr  29435  0uhgrsubgr  29436  chocnul  31487  span0  31701  chsup0  31707  ssnnssfz  32949  xrge0tsmsd  33213  elrgspnlem4  33386  unitprodclb  33535  constrfiss  34008  ddemeas  34493  dya2iocuni  34540  oms0  34554  0elcarsg  34564  eulerpartlemt  34628  bnj1143  35045  mrsubrn  35823  msubrn  35839  mthmpps  35892  bj-nuliotaALT  37503  bj-restsn0  37535  bj-restsn10  37536  bj-imdirco  37642  pibt2  37871  mblfinlem2  38117  mblfinlem3  38118  ismblfin  38120  sstotbnd2  38233  isbnd3  38243  ssbnd  38247  heiborlem6  38275  lub0N  39773  glb0N  39777  0psubN  40333  padd01  40395  padd02  40396  pol0N  40493  pcl0N  40506  0psubclN  40527  mzpcompact2lem  43292  itgocn  43701  oaabsb  43831  oege1  43843  nnoeomeqom  43849  cantnfresb  43861  omabs2  43869  omcl2  43870  tfsconcatb0  43881  nadd2rabex  43923  fpwfvss  43948  nla0002  43960  nla0003  43961  nla0001  43962  fvnonrel  44133  clcnvlem  44159  cnvrcl0  44161  cnvtrcl0  44162  0he  44318  ntrclskb  44605  gru0eld  44765  mnu0eld  44801  mnuprdlem4  44811  mnuprd  44812  founiiun0  45728  uzfissfz  45862  limcdm0  46154  cncfiooicc  46428  itgvol0  46502  ibliooicc  46505  ovn0  47100  sprssspr  48047  isubgr0uhgr  48455  ssnn0ssfz  48931  ipolub0  49573  ipoglb0  49575  discsubc  49645  iinfconstbas  49647  nelsubclem  49648  setc1onsubc  50183  setrec2fun  50273  setrec2mpt  50278