Theorem 0ss 4327

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

Syntax hints:   ∈ wcel 2108   ⊆ wss 3883  ∅c0 4253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886  df-in 3890  df-ss 3900  df-nul 4254

This theorem is referenced by:  ss0b  4328  0pss  4375  npss0  4376  ssdifeq0  4414  pwpw0  4743  sssn  4756  sspr  4763  sstp  4764  pwsnOLD  4829  uni0  4866  int0el  4907  0disj  5062  disjx0  5064  tr0  5198  al0ssb  5227  0elpw  5273  rel0  5698  0ima  5975  dmxpss  6063  dmsnopss  6106  dfpo2  6188  on0eqel  6369  iotassuni  6397  fun0  6483  f0  6639  fvmptss  6869  fvmptss2  6882  funressn  7013  riotassuni  7253  frxp  7938  suppssdm  7964  suppun  7971  suppss  7981  suppssOLD  7982  suppssov1  7985  suppss2  7987  suppssfv  7989  oaword1  8345  oaword2  8346  omwordri  8365  oewordri  8385  oeworde  8386  nnaword1  8422  mapssfset  8597  0domg  8840  fodomr  8864  pwdom  8865  php  8897  isinf  8965  finsschain  9056  fipwuni  9115  fipwss  9118  wdompwdom  9267  inf3lemd  9315  inf3lem1  9316  cantnfle  9359  trpredlem1  9405  tc0  9436  r1val1  9475  alephgeom  9769  infmap2  9905  cfub  9936  cf0  9938  cflecard  9940  cfle  9941  fin23lem16  10022  itunitc1  10107  ttukeylem6  10201  ttukeylem7  10202  canthwe  10338  wun0  10405  tsk0  10450  gruina  10505  grur1a  10506  uzssz  12532  xrsup0  12986  fzoss1  13342  fsuppmapnn0fiubex  13640  swrd00  14285  swrdlend  14294  repswswrd  14425  xptrrel  14619  relexpdmd  14683  relexprnd  14687  relexpfldd  14689  rtrclreclem4  14700  sum0  15361  fsumss  15365  fsumcvg3  15369  prod0  15581  0bits  16074  sadid1  16103  sadid2  16104  smu01lem  16120  smu01  16121  smu02  16122  lcmf0  16267  vdwmc2  16608  vdwlem13  16622  ramz2  16653  strfvss  16816  ressbasss  16876  ress0  16879  ismred2  17229  acsfn  17285  acsfn0  17286  0ssc  17468  fullfunc  17538  fthfunc  17539  mrelatglb0  18194  cntzssv  18849  symgsssg  18990  efgsfo  19260  dprdsn  19554  lsp0  20186  lss0v  20193  lspsnat  20322  lsppratlem3  20326  lbsexg  20341  evpmss  20703  ocv0  20794  ocvz  20795  css1  20807  resspsrbas  21094  mhp0cl  21246  psr1crng  21268  psr1assa  21269  psr1tos  21270  psr1bas2  21271  vr1cl2  21274  ply1lss  21277  ply1subrg  21278  psr1plusg  21303  psr1vsca  21304  psr1mulr  21305  psr1ring  21328  psr1lmod  21330  psr1sca  21331  0opn  21961  toponsspwpw  21979  basdif0  22011  baspartn  22012  0cld  22097  ntr0  22140  cmpfi  22467  refun0  22574  xkouni  22658  xkoccn  22678  alexsubALTlem2  23107  ptcmplem2  23112  tsmsfbas  23187  setsmstopn  23539  restmetu  23632  tngtopn  23720  iccntr  23890  xrge0gsumle  23902  xrge0tsms  23903  metdstri  23920  ovol0  24562  0mbl  24608  itg1le  24783  itgioo  24885  limcnlp  24947  dvbsss  24971  plyssc  25266  fsumharmonic  26066  egrsubgr  27547  0grsubgr  27548  0uhgrsubgr  27549  chocnul  29591  span0  29805  chsup0  29811  ssnnssfz  31010  xrge0tsmsd  31219  ddemeas  32104  dya2iocuni  32150  oms0  32164  0elcarsg  32174  eulerpartlemt  32238  bnj1143  32670  mrsubrn  33375  msubrn  33391  mthmpps  33444  ttrclselem1  33711  nulsslt  33918  nulssgt  33919  bday0b  33951  madess  33986  oldssmade  33987  bj-nuliotaALT  35156  bj-restsn0  35183  bj-restsn10  35184  bj-imdirco  35288  pibt2  35515  mblfinlem2  35742  mblfinlem3  35743  ismblfin  35745  sstotbnd2  35859  isbnd3  35869  ssbnd  35873  heiborlem6  35901  lub0N  37130  glb0N  37134  0psubN  37690  padd01  37752  padd02  37753  pol0N  37850  pcl0N  37863  0psubclN  37884  sn-iotassuni  40122  mzpcompact2lem  40489  itgocn  40905  fvnonrel  41094  clcnvlem  41120  cnvrcl0  41122  cnvtrcl0  41123  0he  41279  ntrclskb  41568  gru0eld  41736  mnu0eld  41772  mnuprdlem4  41782  mnuprd  41783  founiiun0  42617  uzfissfz  42755  limcdm0  43049  cncfiooicc  43325  itgvol0  43399  ibliooicc  43402  ovn0  43994  sprssspr  44821  ssnn0ssfz  45573  ipolub0  46166  ipoglb0  46168  setrec2fun  46284