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

Theorem 0ss 3919
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 3873 . . 3 ¬ 𝑥 ∈ ∅
21pm2.21i 114 . 2 (𝑥 ∈ ∅ → 𝑥𝐴)
32ssriv 3567 1 ∅ ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  wcel 1975  wss 3535  c0 3869
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-v 3170  df-dif 3538  df-in 3542  df-ss 3549  df-nul 3870
This theorem is referenced by:  ss0b  3920  0pss  3960  npss0  3961  npss0OLD  3962  ssdifeq0  3998  pwpw0  4279  sssn  4291  sspr  4297  sstp  4298  pwsnALT  4357  uni0  4391  int0el  4433  0disj  4565  disjx0  4567  tr0  4682  0elpw  4751  rel0  5151  0ima  5384  dmxpss  5466  dmsnopss  5507  on0eqel  5744  iotassuni  5766  fun0  5850  fresaunres2  5970  f0  5980  fvmptss  6182  fvmptss2  6193  funressn  6305  riotassuni  6521  frxp  7147  suppssdm  7168  suppun  7175  suppss  7185  suppssov1  7187  suppss2  7189  suppssfv  7191  oaword1  7492  oaword2  7493  omwordri  7512  oewordri  7532  oeworde  7533  nnaword1  7569  0domg  7945  fodomr  7969  pwdom  7970  php  8002  isinf  8031  finsschain  8129  fipwuni  8188  fipwss  8191  wdompwdom  8339  inf3lemd  8380  inf3lem1  8381  cantnfle  8424  tc0  8479  r1val1  8505  alephgeom  8761  infmap2  8896  cfub  8927  cf0  8929  cflecard  8931  cfle  8932  fin23lem16  9013  itunitc1  9098  ttukeylem6  9192  ttukeylem7  9193  canthwe  9325  wun0  9392  tsk0  9437  gruina  9492  grur1a  9493  uzssz  11535  xrsup0  11977  fzoss1  12315  fsuppmapnn0fiubex  12605  swrd00  13212  swrdlend  13225  swrd0  13228  repswswrd  13324  xptrrel  13509  sum0  14241  fsumss  14245  fsumcvg3  14249  prod0  14454  0bits  14941  sadid1  14970  sadid2  14971  smu01lem  14987  smu01  14988  smu02  14989  lcmf0  15127  vdwmc2  15463  vdwlem13  15477  ramz2  15508  strfvss  15655  ressbasss  15701  ress0  15703  strlemor0  15737  ismred2  16028  acsfn  16085  acsfn0  16086  0ssc  16262  fullfunc  16331  fthfunc  16332  mrelatglb0  16950  cntzssv  17526  symgsssg  17652  efgsfo  17917  dprdsn  18200  lsp0  18772  lss0v  18779  lspsnat  18908  lsppratlem3  18912  lbsexg  18927  resspsrbas  19178  psr1crng  19320  psr1assa  19321  psr1tos  19322  psr1bas2  19323  vr1cl2  19326  ply1lss  19329  ply1subrg  19330  psr1plusg  19355  psr1vsca  19356  psr1mulr  19357  psr1ring  19380  psr1lmod  19382  psr1sca  19383  evpmss  19692  ocv0  19778  ocvz  19779  css1  19791  0opn  20472  basdif0  20506  baspartn  20507  0cld  20590  cls0  20632  ntr0  20633  cmpfi  20959  refun0  21066  xkouni  21150  xkoccn  21170  alexsubALTlem2  21600  ptcmplem2  21605  tsmsfbas  21679  setsmstopn  22030  restmetu  22122  tngtopn  22198  iccntr  22360  xrge0gsumle  22372  xrge0tsms  22373  metdstri  22389  ovol0  22981  0mbl  23027  itg1le  23199  itgioo  23301  limcnlp  23361  dvbsss  23385  plyssc  23673  fsumharmonic  24451  chocnul  27373  span0  27587  chsup0  27593  ssnnssfz  28739  xrge0tsmsd  28918  ddemeas  29428  dya2iocuni  29474  oms0  29488  0elcarsg  29498  eulerpartlemt  29562  bnj1143  29917  mrsubrn  30466  msubrn  30482  mthmpps  30535  dfpo2  30700  trpredlem1  30773  bj-nuliotaALT  32010  bj-restsn0  32018  bj-restsn10  32019  bj-toponss  32040  mblfinlem2  32416  mblfinlem3  32417  ismblfin  32419  sstotbnd2  32542  isbnd3  32552  ssbnd  32556  heiborlem6  32584  lub0N  33293  glb0N  33297  0psubN  33852  padd01  33914  padd02  33915  pol0N  34012  pcl0N  34025  0psubclN  34046  mzpcompact2lem  36131  itgocn  36552  fvnonrel  36721  clcnvlem  36748  cnvrcl0  36750  cnvtrcl0  36751  0he  36895  ntrclskb  37186  founiiun0  38171  uzfissfz  38283  limcdm0  38485  cncfiooicc  38580  itgvol0  38660  ibliooicc  38663  ovn0  39256  egrsubgr  40499  0grsubgr  40500  0uhgrsubgr  40501  ssnn0ssfz  41918
  Copyright terms: Public domain W3C validator