MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  0ss Structured version   Visualization version   GIF version

Theorem 0ss 4111
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.
StepHypRef Expression
1 noel 4058 . . 3 ¬ 𝑥 ∈ ∅
21pm2.21i 116 . 2 (𝑥 ∈ ∅ → 𝑥𝐴)
32ssriv 3744 1 ∅ ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  wcel 2135  wss 3711  c0 4054
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-v 3338  df-dif 3714  df-in 3718  df-ss 3725  df-nul 4055
This theorem is referenced by:  ss0b  4112  0pss  4152  npss0  4153  npss0OLD  4154  ssdifeq0  4191  pwpw0  4485  sssn  4499  sspr  4507  sstp  4508  pwsnALT  4577  uni0  4613  int0el  4656  0disj  4793  disjx0  4795  tr0  4912  0elpw  4979  rel0  5395  0ima  5636  dmxpss  5719  dmsnopss  5762  on0eqel  6002  iotassuni  6024  fun0  6111  fresaunres2  6233  f0  6243  fvmptss  6450  fvmptss2  6462  funressn  6585  riotassuni  6807  frxp  7451  suppssdm  7472  suppun  7479  suppss  7490  suppssov1  7492  suppss2  7494  suppssfv  7496  oaword1  7797  oaword2  7798  omwordri  7817  oewordri  7837  oeworde  7838  nnaword1  7874  0domg  8248  fodomr  8272  pwdom  8273  php  8305  isinf  8334  finsschain  8434  fipwuni  8493  fipwss  8496  wdompwdom  8644  inf3lemd  8693  inf3lem1  8694  cantnfle  8737  tc0  8792  r1val1  8818  alephgeom  9091  infmap2  9228  cfub  9259  cf0  9261  cflecard  9263  cfle  9264  fin23lem16  9345  itunitc1  9430  ttukeylem6  9524  ttukeylem7  9525  canthwe  9661  wun0  9728  tsk0  9773  gruina  9828  grur1a  9829  uzssz  11895  xrsup0  12342  fzoss1  12685  fsuppmapnn0fiubex  12982  swrd00  13613  swrdlend  13627  swrd0  13630  repswswrd  13727  xptrrel  13916  sum0  14647  fsumss  14651  fsumcvg3  14655  prod0  14868  0bits  15359  sadid1  15388  sadid2  15389  smu01lem  15405  smu01  15406  smu02  15407  lcmf0  15545  vdwmc2  15881  vdwlem13  15895  ramz2  15926  strfvss  16078  ressbasss  16130  ress0  16132  strlemor0OLD  16166  ismred2  16461  acsfn  16517  acsfn0  16518  0ssc  16694  fullfunc  16763  fthfunc  16764  mrelatglb0  17382  cntzssv  17957  symgsssg  18083  efgsfo  18348  dprdsn  18631  lsp0  19207  lss0v  19214  lspsnat  19343  lsppratlem3  19347  lbsexg  19362  resspsrbas  19613  psr1crng  19755  psr1assa  19756  psr1tos  19757  psr1bas2  19758  vr1cl2  19761  ply1lss  19764  ply1subrg  19765  psr1plusg  19790  psr1vsca  19791  psr1mulr  19792  psr1ring  19815  psr1lmod  19817  psr1sca  19818  evpmss  20130  ocv0  20219  ocvz  20220  css1  20232  0opn  20907  toponsspwpw  20924  basdif0  20955  baspartn  20956  0cld  21040  cls0  21082  ntr0  21083  cmpfi  21409  refun0  21516  xkouni  21600  xkoccn  21620  alexsubALTlem2  22049  ptcmplem2  22054  tsmsfbas  22128  setsmstopn  22480  restmetu  22572  tngtopn  22651  iccntr  22821  xrge0gsumle  22833  xrge0tsms  22834  metdstri  22851  ovol0  23457  0mbl  23503  itg1le  23675  itgioo  23777  limcnlp  23837  dvbsss  23861  plyssc  24151  fsumharmonic  24933  egrsubgr  26364  0grsubgr  26365  0uhgrsubgr  26366  chocnul  28492  span0  28706  chsup0  28712  ssnnssfz  29854  xrge0tsmsd  30090  ddemeas  30604  dya2iocuni  30650  oms0  30664  0elcarsg  30674  eulerpartlemt  30738  bnj1143  31164  mrsubrn  31713  msubrn  31729  mthmpps  31782  dfpo2  31948  trpredlem1  32028  nulsslt  32210  nulssgt  32211  bj-nuliotaALT  33322  bj-restsn0  33340  bj-restsn10  33341  bj-ismooredr2  33367  mblfinlem2  33756  mblfinlem3  33757  ismblfin  33759  sstotbnd2  33882  isbnd3  33892  ssbnd  33896  heiborlem6  33924  lub0N  34975  glb0N  34979  0psubN  35534  padd01  35596  padd02  35597  pol0N  35694  pcl0N  35707  0psubclN  35728  mzpcompact2lem  37812  itgocn  38232  fvnonrel  38401  clcnvlem  38428  cnvrcl0  38430  cnvtrcl0  38431  0he  38574  ntrclskb  38865  founiiun0  39872  uzfissfz  40036  limcdm0  40349  cncfiooicc  40606  itgvol0  40683  ibliooicc  40686  ovn0  41282  sprssspr  42237  ssnn0ssfz  42633  setrec2fun  42945
  Copyright terms: Public domain W3C validator