Theorem 0ss 4349

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

This proof depends on syntax axioms:   ∈ wcel 2144   ⊆ wss 3895  ∅c0 4278

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3896  df-dif 4047  df-nul 4279

This theorem is used by:  ss0b  4350  0pss  4359  npss0  4360  ssdifeq0  4441  sssn  4781  sspr  4789  sstp  4790  pwpw0  4830  uni0OLD  4896  int0el  4938  0disj  5095  disjx0  5097  tr0  5224  al0ssb  5261  0elpw  5316  rel0  5775  dmxpss  6162  0ima  6200  dmsnopss  6215  dfpo2  6299  on0eqel  6488  iotassuni  6513  fun0  6606  f0  6764  fvmptss  7007  fvmptss2  7021  funressn  7164  riotassuni  7418  ordsuci  7823  frxp  8141  suppssdm  8198  suppun  8205  suppss  8215  suppssov1  8218  suppssov2  8219  suppss2  8221  suppssfv  8223  oaword1  8564  oaword2  8565  omwordri  8584  oewordri  8605  oeworde  8606  nnaword1  8642  naddword1  8705  mapssfset  8877  fodomr  9151  pwdom  9152  php  9226  isinf  9260  fodomfir  9323  finsschain  9352  fipwuni  9422  fipwss  9425  wdompwdom  9576  inf3lemd  9632  inf3lem1  9633  cantnfle  9676  ttrclselem1  9730  tc0  9750  r1val1  9797  setrec2fun  9977  alephgeom  10165  infmap2  10299  cfub  10330  cf0  10332  cflecard  10334  cfle  10335  fin23lem16  10417  itunitc1  10502  ttukeylem6  10596  ttukeylem7  10597  canthwe  10740  wun0  10807  tsk0  10852  gruina  10907  grur1a  10908  indconst0  12336  uzssz  12990  xrsup0  13457  fzoss1  13825  fsuppmapnn0fiubex  14139  swrd00  14797  swrdlend  14808  repswswrd  14940  xptrrel  15139  relexpdmd  15203  relexprnd  15207  relexpfldd  15209  rtrclreclem4  15220  sum0  15893  fsumss  15897  fsumcvg3  15901  prod0  16116  0bits  16615  sadid1  16644  sadid2  16645  smu01lem  16661  smu01  16662  smu02  16663  lcmf0  16815  vdwmc2  17163  vdwlem13  17177  ramz2  17208  strfvss  17371  ressbasssg  17421  ressbasssOLD  17424  ress0  17427  ismred2  17779  acsfn  17839  acsfn0  17840  0ssc  18018  fullfunc  18089  fthfunc  18090  mrelatglb0  18741  cntzssv  19548  symgsssg  19687  efgsfo  19959  dprdsn  20258  lsp0  21290  lss0v  21297  lspsnat  21429  lsppratlem3  21433  lbsexg  21448  evpmss  21898  ocv0  21989  ocvz  21990  css1  22002  resspsrbas  22287  mhp0cl  22473  psr1crng  22511  psr1assa  22512  psr1tos  22513  psr1bas2  22514  vr1cl2  22517  ply1lss  22520  ply1subrg  22521  psr1plusg  22544  psr1vsca  22545  psr1mulr  22546  psr1ring  22570  psr1lmod  22572  psr1sca  22573  0opn  23228  toponsspwpw  23246  basdif0  23277  baspartn  23278  0cld  23362  ntr0  23405  cmpfi  23732  refun0  23840  xkouni  23924  xkoccn  23944  alexsubALTlem2  24373  ptcmplem2  24378  tsmsfbas  24453  setsmstopn  24803  restmetu  24895  tngtopn  24975  iccntr  25147  xrge0gsumle  25159  xrge0tsms  25160  metdstri  25177  ovol0  25820  0mbl  25866  itg1le  26040  itgioo  26142  limcnlp  26204  dvbsss  26228  plyssc  26524  fsumharmonic  27345  nulslts  28167  nulsgts  28168  bday0b  28205  madess  28258  oldssmade  28259  oldss  28262  precsexlem8  28606  bdaypw2n0bndlem  28855  bdaypw2n0bnd  28856  egrsubgr  29864  0grsubgr  29865  0uhgrsubgr  29866  chocnul  31936  span0  32150  chsup0  32156  ssnnssfz  33426  xrge0tsmsd  33681  elrgspnlem4  33853  unitprodclb  33991  constrfiss  34430  ddemeas  34916  dya2iocuni  34962  oms0  34976  0elcarsg  34986  eulerpartlemt  35050  bnj1143  35467  rankscottu  35808  rankkardu  35896  mrsubrn  36365  msubrn  36381  mthmpps  36434  nmulss1  37056  bj-nuliotaALT  38066  bj-restsn0  38099  bj-restsn10  38100  bj-pr0moore  38130  bj-imdirco  38205  pibt2  38434  mblfinlem2  38670  mblfinlem3  38671  ismblfin  38673  varprop  38736  sstotbnd2  38802  isbnd3  38812  ssbnd  38816  heiborlem6  38844  lub0N  40340  glb0N  40344  0psubN  40900  padd01  40962  padd02  40963  pol0N  41060  pcl0N  41073  0psubclN  41094  mzpcompact2lem  43856  itgocn  44260  oaabsb  44390  oege1  44402  nnoeomeqom  44408  cantnfresb  44420  omabs2  44428  omcl2  44429  tfsconcatb0  44440  nadd2rabex  44482  fpwfvss  44507  nla0002  44519  nla0003  44520  nla0001  44521  fvnonrel  44691  clcnvlem  44717  cnvrcl0  44719  cnvtrcl0  44720  0he  44876  ntrclskb  45163  gru0eld  45321  mnu0eld  45343  mnuprdlem4  45353  mnuprd  45354  founiiun0  46299  uzfissfz  46432  limcdm0  46724  cncfiooicc  46998  itgvol0  47072  ibliooicc  47075  ovn0  47670  sprssspr  48657  isubgr0uhgr  49065  ssnn0ssfz  49555  ipolub0  50200  ipoglb0  50202  discsubc  50272  iinfconstbas  50274  nelsubclem  50275  setc1onsubc  50834  setrec2mpt  50959