Theorem 0ss 4358

Description: The empty set is a subset of any class. Dual of ssv 3962. 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 4292	. . 3 ⊢ ¬ 𝑥 ∈ ∅
2	1	pm2.21i 120	. 2 ⊢ (𝑥 ∈ ∅ → 𝑥 ∈ 𝐴)
3	2	ssriv 3942	1 ⊢ ∅ ⊆ 𝐴

Syntax hints:   ∈ wcel 2143   ⊆ wss 3906  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-dif 3909  df-ss 3923  df-nul 4288

This theorem is referenced by:  ss0b  4359  0pss  4368  npss0  4369  ssdifeq0  4448  pwpw0  4780  sssn  4793  sspr  4801  sstp  4802  uni0OLD  4903  int0el  4945  0disj  5103  disjx0  5105  tr0  5232  al0ssb  5272  0elpw  5328  rel0  5787  0ima  6082  dmxpss  6171  dmsnopss  6217  dfpo2  6299  on0eqel  6488  iotassuni  6513  fun0  6603  f0  6761  fvmptss  7004  fvmptss2  7018  funressn  7158  riotassuni  7409  ordsuci  7808  frxp  8123  suppssdm  8174  suppun  8181  suppss  8191  suppssov1  8194  suppssov2  8195  suppss2  8197  suppssfv  8199  oaword1  8538  oaword2  8539  omwordri  8558  oewordri  8579  oeworde  8580  nnaword1  8616  naddword1  8679  mapssfset  8849  fodomr  9117  pwdom  9118  php  9192  isinf  9226  fodomfir  9288  finsschain  9317  fipwuni  9387  fipwss  9390  wdompwdom  9541  inf3lemd  9597  inf3lem1  9598  cantnfle  9641  ttrclselem1  9695  tc0  9715  r1val1  9759  alephgeom  10067  infmap2  10201  cfub  10233  cf0  10235  cflecard  10237  cfle  10238  fin23lem16  10320  itunitc1  10405  ttukeylem6  10499  ttukeylem7  10500  canthwe  10637  wun0  10704  tsk0  10749  gruina  10804  grur1a  10805  indconst0  12231  uzssz  12884  xrsup0  13350  fzoss1  13717  fsuppmapnn0fiubex  14030  swrd00  14684  swrdlend  14693  repswswrd  14823  xptrrel  15019  relexpdmd  15083  relexprnd  15087  relexpfldd  15089  rtrclreclem4  15100  sum0  15774  fsumss  15778  fsumcvg3  15782  prod0  15999  0bits  16498  sadid1  16527  sadid2  16528  smu01lem  16544  smu01  16545  smu02  16546  lcmf0  16693  vdwmc2  17040  vdwlem13  17054  ramz2  17085  strfvss  17248  ressbasssg  17298  ressbasssOLD  17301  ress0  17304  ismred2  17656  acsfn  17716  acsfn0  17717  0ssc  17895  fullfunc  17966  fthfunc  17967  mrelatglb0  18618  cntzssv  19399  symgsssg  19538  efgsfo  19810  dprdsn  20109  lsp0  21111  lss0v  21118  lspsnat  21250  lsppratlem3  21254  lbsexg  21269  evpmss  21717  ocv0  21808  ocvz  21809  css1  21821  resspsrbas  22104  mhp0cl  22290  psr1crng  22328  psr1assa  22329  psr1tos  22330  psr1bas2  22331  vr1cl2  22334  ply1lss  22337  ply1subrg  22338  psr1plusg  22361  psr1vsca  22362  psr1mulr  22363  psr1ring  22387  psr1lmod  22389  psr1sca  22390  0opn  23042  toponsspwpw  23060  basdif0  23091  baspartn  23092  0cld  23176  ntr0  23219  cmpfi  23546  refun0  23653  xkouni  23737  xkoccn  23757  alexsubALTlem2  24186  ptcmplem2  24191  tsmsfbas  24266  setsmstopn  24616  restmetu  24708  tngtopn  24788  iccntr  24960  xrge0gsumle  24972  xrge0tsms  24973  metdstri  24990  ovol0  25633  0mbl  25679  itg1le  25853  itgioo  25956  limcnlp  26018  dvbsss  26042  plyssc  26338  fsumharmonic  27157  nulslts  27949  nulsgts  27950  bday0b  27987  madess  28040  oldssmade  28041  oldss  28044  precsexlem8  28388  bdaypw2n0bndlem  28637  bdaypw2n0bnd  28638  egrsubgr  29608  0grsubgr  29609  0uhgrsubgr  29610  chocnul  31661  span0  31875  chsup0  31881  ssnnssfz  33113  xrge0tsmsd  33374  elrgspnlem4  33546  unitprodclb  33683  constrfiss  34122  ddemeas  34607  dya2iocuni  34654  oms0  34668  0elcarsg  34678  eulerpartlemt  34742  bnj1143  35159  rankscottu  35504  rankkardu  35565  mrsubrn  35986  msubrn  36002  mthmpps  36055  nmulss1  36672  bj-nuliotaALT  37675  bj-restsn0  37708  bj-restsn10  37709  bj-imdirco  37815  pibt2  38044  mblfinlem2  38290  mblfinlem3  38291  ismblfin  38293  sstotbnd2  38406  isbnd3  38416  ssbnd  38420  heiborlem6  38448  lub0N  39944  glb0N  39948  0psubN  40504  padd01  40566  padd02  40567  pol0N  40664  pcl0N  40677  0psubclN  40698  mzpcompact2lem  43465  itgocn  43874  oaabsb  44004  oege1  44016  nnoeomeqom  44022  cantnfresb  44034  omabs2  44042  omcl2  44043  tfsconcatb0  44054  nadd2rabex  44096  fpwfvss  44121  nla0002  44133  nla0003  44134  nla0001  44135  fvnonrel  44306  clcnvlem  44332  cnvrcl0  44334  cnvtrcl0  44335  0he  44491  ntrclskb  44778  gru0eld  44936  mnu0eld  44958  mnuprdlem4  44968  mnuprd  44969  founiiun0  45891  uzfissfz  46025  limcdm0  46317  cncfiooicc  46591  itgvol0  46665  ibliooicc  46668  ovn0  47263  sprssspr  48213  isubgr0uhgr  48621  ssnn0ssfz  49112  ipolub0  49753  ipoglb0  49755  discsubc  49825  iinfconstbas  49827  nelsubclem  49828  setc1onsubc  50363  setrec2fun  50453  setrec2mpt  50458