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

Theorem 0ss 3970
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 3917 . . 3 ¬ 𝑥 ∈ ∅
21pm2.21i 116 . 2 (𝑥 ∈ ∅ → 𝑥𝐴)
32ssriv 3605 1 ∅ ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  wcel 1989  wss 3572  c0 3913
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-v 3200  df-dif 3575  df-in 3579  df-ss 3586  df-nul 3914
This theorem is referenced by:  ss0b  3971  0pss  4011  npss0  4012  npss0OLD  4013  ssdifeq0  4049  pwpw0  4342  sssn  4356  sspr  4364  sstp  4365  pwsnALT  4427  uni0  4463  int0el  4506  0disj  4643  disjx0  4645  tr0  4762  0elpw  4832  rel0  5241  0ima  5480  dmxpss  5563  dmsnopss  5605  on0eqel  5843  iotassuni  5865  fun0  5952  fresaunres2  6074  f0  6084  fvmptss  6290  fvmptss2  6302  funressn  6423  riotassuni  6645  frxp  7284  suppssdm  7305  suppun  7312  suppss  7322  suppssov1  7324  suppss2  7326  suppssfv  7328  oaword1  7629  oaword2  7630  omwordri  7649  oewordri  7669  oeworde  7670  nnaword1  7706  0domg  8084  fodomr  8108  pwdom  8109  php  8141  isinf  8170  finsschain  8270  fipwuni  8329  fipwss  8332  wdompwdom  8480  inf3lemd  8521  inf3lem1  8522  cantnfle  8565  tc0  8620  r1val1  8646  alephgeom  8902  infmap2  9037  cfub  9068  cf0  9070  cflecard  9072  cfle  9073  fin23lem16  9154  itunitc1  9239  ttukeylem6  9333  ttukeylem7  9334  canthwe  9470  wun0  9537  tsk0  9582  gruina  9637  grur1a  9638  uzssz  11704  xrsup0  12150  fzoss1  12491  fsuppmapnn0fiubex  12787  swrd00  13412  swrdlend  13425  swrd0  13428  repswswrd  13525  xptrrel  13713  sum0  14446  fsumss  14450  fsumcvg3  14454  prod0  14667  0bits  15155  sadid1  15184  sadid2  15185  smu01lem  15201  smu01  15202  smu02  15203  lcmf0  15341  vdwmc2  15677  vdwlem13  15691  ramz2  15722  strfvss  15874  ressbasss  15926  ress0  15928  strlemor0OLD  15962  ismred2  16257  acsfn  16314  acsfn0  16315  0ssc  16491  fullfunc  16560  fthfunc  16561  mrelatglb0  17179  cntzssv  17755  symgsssg  17881  efgsfo  18146  dprdsn  18429  lsp0  19003  lss0v  19010  lspsnat  19139  lsppratlem3  19143  lbsexg  19158  resspsrbas  19409  psr1crng  19551  psr1assa  19552  psr1tos  19553  psr1bas2  19554  vr1cl2  19557  ply1lss  19560  ply1subrg  19561  psr1plusg  19586  psr1vsca  19587  psr1mulr  19588  psr1ring  19611  psr1lmod  19613  psr1sca  19614  evpmss  19926  ocv0  20015  ocvz  20016  css1  20028  0opn  20703  toponsspwpw  20720  basdif0  20751  baspartn  20752  0cld  20836  cls0  20878  ntr0  20879  cmpfi  21205  refun0  21312  xkouni  21396  xkoccn  21416  alexsubALTlem2  21846  ptcmplem2  21851  tsmsfbas  21925  setsmstopn  22277  restmetu  22369  tngtopn  22448  iccntr  22618  xrge0gsumle  22630  xrge0tsms  22631  metdstri  22648  ovol0  23255  0mbl  23301  itg1le  23474  itgioo  23576  limcnlp  23636  dvbsss  23660  plyssc  23950  fsumharmonic  24732  egrsubgr  26163  0grsubgr  26164  0uhgrsubgr  26165  chocnul  28171  span0  28385  chsup0  28391  ssnnssfz  29534  xrge0tsmsd  29770  ddemeas  30284  dya2iocuni  30330  oms0  30344  0elcarsg  30354  eulerpartlemt  30418  bnj1143  30846  mrsubrn  31395  msubrn  31411  mthmpps  31464  dfpo2  31631  trpredlem1  31711  nulsslt  31892  nulssgt  31893  bj-nuliotaALT  33004  bj-restsn0  33022  bj-restsn10  33023  bj-ismooredr2  33049  mblfinlem2  33427  mblfinlem3  33428  ismblfin  33430  sstotbnd2  33553  isbnd3  33563  ssbnd  33567  heiborlem6  33595  lub0N  34302  glb0N  34306  0psubN  34861  padd01  34923  padd02  34924  pol0N  35021  pcl0N  35034  0psubclN  35055  mzpcompact2lem  37140  itgocn  37560  fvnonrel  37729  clcnvlem  37756  cnvrcl0  37758  cnvtrcl0  37759  0he  37902  ntrclskb  38193  founiiun0  39199  uzfissfz  39361  limcdm0  39656  cncfiooicc  39876  itgvol0  39953  ibliooicc  39956  ovn0  40549  sprssspr  41502  ssnn0ssfz  41898  setrec2fun  42210
  Copyright terms: Public domain W3C validator