Theorem 0ss 4398

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

Syntax hints:   ∈ wcel 2098   ⊆ wss 3944  ∅c0 4322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-dif 3947  df-ss 3961  df-nul 4323

This theorem is referenced by:  ss0b  4399  0pss  4446  npss0  4447  ssdifeq0  4488  pwpw0  4818  sssn  4831  sspr  4838  sstp  4839  uni0  4939  int0el  4983  0disj  5141  disjx0  5143  tr0  5279  al0ssb  5309  0elpw  5356  rel0  5801  0ima  6082  dmxpss  6177  dmsnopss  6220  dfpo2  6302  on0eqel  6495  iotassuni  6521  iotassuniOLD  6528  fun0  6619  f0  6778  fvmptss  7016  fvmptss2  7030  funressn  7168  riotassuni  7416  ordsuci  7812  frxp  8131  suppssdm  8182  suppun  8189  suppss  8199  suppssOLD  8200  suppssov1  8203  suppssov2  8204  suppss2  8206  suppssfv  8208  oaword1  8573  oaword2  8574  omwordri  8593  oewordri  8613  oeworde  8614  nnaword1  8650  naddword1  8712  mapssfset  8870  0domgOLD  9126  fodomr  9153  pwdom  9154  php  9235  phpOLD  9247  isinf  9285  isinfOLD  9286  finsschain  9385  fipwuni  9451  fipwss  9454  wdompwdom  9603  inf3lemd  9652  inf3lem1  9653  cantnfle  9696  ttrclselem1  9750  tc0  9772  r1val1  9811  alephgeom  10107  infmap2  10243  cfub  10274  cf0  10276  cflecard  10278  cfle  10279  fin23lem16  10360  itunitc1  10445  ttukeylem6  10539  ttukeylem7  10540  canthwe  10676  wun0  10743  tsk0  10788  gruina  10843  grur1a  10844  uzssz  12876  xrsup0  13337  fzoss1  13694  fsuppmapnn0fiubex  13993  swrd00  14630  swrdlend  14639  repswswrd  14770  xptrrel  14963  relexpdmd  15027  relexprnd  15031  relexpfldd  15033  rtrclreclem4  15044  sum0  15703  fsumss  15707  fsumcvg3  15711  prod0  15923  0bits  16417  sadid1  16446  sadid2  16447  smu01lem  16463  smu01  16464  smu02  16465  lcmf0  16608  vdwmc2  16951  vdwlem13  16965  ramz2  16996  strfvss  17159  ressbasssg  17220  ressbasssOLD  17223  ress0  17227  ismred2  17586  acsfn  17642  acsfn0  17643  0ssc  17826  fullfunc  17898  fthfunc  17899  mrelatglb0  18556  cntzssv  19291  symgsssg  19434  efgsfo  19706  dprdsn  20005  lsp0  20905  lss0v  20913  lspsnat  21045  lsppratlem3  21049  lbsexg  21064  evpmss  21535  ocv0  21626  ocvz  21627  css1  21639  resspsrbas  21936  mhp0cl  22093  psr1crng  22129  psr1assa  22130  psr1tos  22131  psr1bas2  22132  vr1cl2  22135  ply1lss  22139  ply1subrg  22140  psr1plusg  22163  psr1vsca  22164  psr1mulr  22165  psr1ring  22189  psr1lmod  22191  psr1sca  22192  0opn  22850  toponsspwpw  22868  basdif0  22900  baspartn  22901  0cld  22986  ntr0  23029  cmpfi  23356  refun0  23463  xkouni  23547  xkoccn  23567  alexsubALTlem2  23996  ptcmplem2  24001  tsmsfbas  24076  setsmstopn  24430  restmetu  24523  tngtopn  24611  iccntr  24781  xrge0gsumle  24793  xrge0tsms  24794  metdstri  24811  ovol0  25466  0mbl  25512  itg1le  25687  itgioo  25789  limcnlp  25851  dvbsss  25875  plyssc  26179  fsumharmonic  26989  nulsslt  27776  nulssgt  27777  bday0b  27809  madess  27849  oldssmade  27850  precsexlem8  28162  egrsubgr  29162  0grsubgr  29163  0uhgrsubgr  29164  chocnul  31210  span0  31424  chsup0  31430  ssnnssfz  32637  xrge0tsmsd  32861  unitprodclb  33201  ddemeas  33986  dya2iocuni  34034  oms0  34048  0elcarsg  34058  eulerpartlemt  34122  bnj1143  34552  mrsubrn  35254  msubrn  35270  mthmpps  35323  bj-nuliotaALT  36668  bj-restsn0  36695  bj-restsn10  36696  bj-imdirco  36800  pibt2  37027  mblfinlem2  37262  mblfinlem3  37263  ismblfin  37265  sstotbnd2  37378  isbnd3  37388  ssbnd  37392  heiborlem6  37420  lub0N  38791  glb0N  38795  0psubN  39352  padd01  39414  padd02  39415  pol0N  39512  pcl0N  39525  0psubclN  39546  mzpcompact2lem  42313  itgocn  42730  oaabsb  42865  oege1  42877  nnoeomeqom  42883  cantnfresb  42895  omabs2  42903  omcl2  42904  tfsconcatb0  42915  nadd2rabex  42957  fpwfvss  42984  nla0002  42996  nla0003  42997  nla0001  42998  fvnonrel  43169  clcnvlem  43195  cnvrcl0  43197  cnvtrcl0  43198  0he  43354  ntrclskb  43641  gru0eld  43808  mnu0eld  43844  mnuprdlem4  43854  mnuprd  43855  founiiun0  44702  uzfissfz  44846  limcdm0  45144  cncfiooicc  45420  itgvol0  45494  ibliooicc  45497  ovn0  46092  sprssspr  46958  isubgr0uhgr  47343  ssnn0ssfz  47599  ipolub0  48189  ipoglb0  48191  setrec2fun  48309  setrec2mpt  48314