Theorem 0ss 4397

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

Syntax hints:   ∈ wcel 2107   ⊆ wss 3949  ∅c0 4323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3952  df-in 3956  df-ss 3966  df-nul 4324

This theorem is referenced by:  ss0b  4398  0pss  4445  npss0  4446  ssdifeq0  4487  pwpw0  4817  sssn  4830  sspr  4837  sstp  4838  pwsnOLD  4902  uni0  4940  int0el  4984  0disj  5141  disjx0  5143  tr0  5279  al0ssb  5309  0elpw  5355  rel0  5800  0ima  6078  dmxpss  6171  dmsnopss  6214  dfpo2  6296  on0eqel  6489  iotassuni  6516  iotassuniOLD  6523  fun0  6614  f0  6773  fvmptss  7011  fvmptss2  7024  funressn  7157  riotassuni  7406  ordsuci  7796  frxp  8112  suppssdm  8162  suppun  8169  suppss  8179  suppssOLD  8180  suppssov1  8183  suppss2  8185  suppssfv  8187  oaword1  8552  oaword2  8553  omwordri  8572  oewordri  8592  oeworde  8593  nnaword1  8629  naddword1  8690  mapssfset  8845  0domgOLD  9101  fodomr  9128  pwdom  9129  php  9210  phpOLD  9222  isinf  9260  isinfOLD  9261  finsschain  9359  fipwuni  9421  fipwss  9424  wdompwdom  9573  inf3lemd  9622  inf3lem1  9623  cantnfle  9666  ttrclselem1  9720  tc0  9742  r1val1  9781  alephgeom  10077  infmap2  10213  cfub  10244  cf0  10246  cflecard  10248  cfle  10249  fin23lem16  10330  itunitc1  10415  ttukeylem6  10509  ttukeylem7  10510  canthwe  10646  wun0  10713  tsk0  10758  gruina  10813  grur1a  10814  uzssz  12843  xrsup0  13302  fzoss1  13659  fsuppmapnn0fiubex  13957  swrd00  14594  swrdlend  14603  repswswrd  14734  xptrrel  14927  relexpdmd  14991  relexprnd  14995  relexpfldd  14997  rtrclreclem4  15008  sum0  15667  fsumss  15671  fsumcvg3  15675  prod0  15887  0bits  16380  sadid1  16409  sadid2  16410  smu01lem  16426  smu01  16427  smu02  16428  lcmf0  16571  vdwmc2  16912  vdwlem13  16926  ramz2  16957  strfvss  17120  ressbasssg  17181  ressbasssOLD  17184  ress0  17188  ismred2  17547  acsfn  17603  acsfn0  17604  0ssc  17787  fullfunc  17857  fthfunc  17858  mrelatglb0  18514  cntzssv  19192  symgsssg  19335  efgsfo  19607  dprdsn  19906  lsp0  20620  lss0v  20627  lspsnat  20758  lsppratlem3  20762  lbsexg  20777  evpmss  21139  ocv0  21230  ocvz  21231  css1  21243  resspsrbas  21535  mhp0cl  21689  psr1crng  21711  psr1assa  21712  psr1tos  21713  psr1bas2  21714  vr1cl2  21717  ply1lss  21720  ply1subrg  21721  psr1plusg  21744  psr1vsca  21745  psr1mulr  21746  psr1ring  21769  psr1lmod  21771  psr1sca  21772  0opn  22406  toponsspwpw  22424  basdif0  22456  baspartn  22457  0cld  22542  ntr0  22585  cmpfi  22912  refun0  23019  xkouni  23103  xkoccn  23123  alexsubALTlem2  23552  ptcmplem2  23557  tsmsfbas  23632  setsmstopn  23986  restmetu  24079  tngtopn  24167  iccntr  24337  xrge0gsumle  24349  xrge0tsms  24350  metdstri  24367  ovol0  25010  0mbl  25056  itg1le  25231  itgioo  25333  limcnlp  25395  dvbsss  25419  plyssc  25714  fsumharmonic  26516  nulsslt  27298  nulssgt  27299  bday0b  27331  madess  27371  oldssmade  27372  precsexlem8  27660  egrsubgr  28534  0grsubgr  28535  0uhgrsubgr  28536  chocnul  30581  span0  30795  chsup0  30801  ssnnssfz  31998  xrge0tsmsd  32209  ddemeas  33234  dya2iocuni  33282  oms0  33296  0elcarsg  33306  eulerpartlemt  33370  bnj1143  33801  mrsubrn  34504  msubrn  34520  mthmpps  34573  bj-nuliotaALT  35939  bj-restsn0  35966  bj-restsn10  35967  bj-imdirco  36071  pibt2  36298  mblfinlem2  36526  mblfinlem3  36527  ismblfin  36529  sstotbnd2  36642  isbnd3  36652  ssbnd  36656  heiborlem6  36684  lub0N  38059  glb0N  38063  0psubN  38620  padd01  38682  padd02  38683  pol0N  38780  pcl0N  38793  0psubclN  38814  mzpcompact2lem  41489  itgocn  41906  oaabsb  42044  oege1  42056  nnoeomeqom  42062  cantnfresb  42074  omabs2  42082  omcl2  42083  tfsconcatb0  42094  nadd2rabex  42136  fpwfvss  42163  nla0002  42175  nla0003  42176  nla0001  42177  fvnonrel  42348  clcnvlem  42374  cnvrcl0  42376  cnvtrcl0  42377  0he  42533  ntrclskb  42820  gru0eld  42988  mnu0eld  43024  mnuprdlem4  43034  mnuprd  43035  founiiun0  43888  uzfissfz  44036  limcdm0  44334  cncfiooicc  44610  itgvol0  44684  ibliooicc  44687  ovn0  45282  sprssspr  46149  ssnn0ssfz  47025  ipolub0  47617  ipoglb0  47619  setrec2fun  47737  setrec2mpt  47742