MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  metxmet Structured version   Unicode version

Theorem metxmet 19931
Description: A metric is an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015.)
Assertion
Ref Expression
metxmet  |-  ( D  e.  ( Met `  X
)  ->  D  e.  ( *Met `  X
) )

Proof of Theorem metxmet
StepHypRef Expression
1 ismet2 19930 . 2  |-  ( D  e.  ( Met `  X
)  <->  ( D  e.  ( *Met `  X )  /\  D : ( X  X.  X ) --> RR ) )
21simplbi 460 1  |-  ( D  e.  ( Met `  X
)  ->  D  e.  ( *Met `  X
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756    X. cxp 4859   -->wf 5435   ` cfv 5439   RRcr 9302   *Metcxmt 17823   Metcme 17824
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4434  ax-nul 4442  ax-pow 4491  ax-pr 4552  ax-un 6393  ax-cnex 9359  ax-resscn 9360  ax-1cn 9361  ax-icn 9362  ax-addcl 9363  ax-mulcl 9365  ax-i2m1 9371
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-nel 2623  df-ral 2741  df-rex 2742  df-rab 2745  df-v 2995  df-sbc 3208  df-csb 3310  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-pw 3883  df-sn 3899  df-pr 3901  df-op 3905  df-uni 4113  df-br 4314  df-opab 4372  df-mpt 4373  df-id 4657  df-xp 4867  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-rn 4872  df-res 4873  df-ima 4874  df-iota 5402  df-fun 5441  df-fn 5442  df-f 5443  df-f1 5444  df-fo 5445  df-f1o 5446  df-fv 5447  df-ov 6115  df-oprab 6116  df-mpt2 6117  df-er 7122  df-map 7237  df-en 7332  df-dom 7333  df-sdom 7334  df-pnf 9441  df-mnf 9442  df-xr 9443  df-xadd 11111  df-xmet 17832  df-met 17833
This theorem is referenced by:  metdmdm  19933  meteq0  19936  mettri2  19938  met0  19940  metge0  19942  metsym  19947  metrtri  19954  metgt0  19956  metres2  19960  prdsmet  19967  imasf1omet  19973  blpnf  19994  bl2in  19997  isms2  20047  setsms  20077  tmsms  20084  metss2lem  20108  metss2  20109  methaus  20117  dscopn  20188  cnxmet  20374  rexmet  20390  metdcn2  20438  metdsre  20451  metdscn2  20455  lebnumlem1  20555  lebnumlem2  20556  lebnumlem3  20557  lebnum  20558  xlebnum  20559  cmetcaulem  20821  cmetcau  20822  iscmet3lem1  20824  iscmet3lem2  20825  iscmet3  20826  equivcfil  20832  equivcau  20833  cmetss  20847  relcmpcmet  20849  cmpcmet  20850  cncmet  20855  bcthlem2  20858  bcthlem3  20859  bcthlem4  20860  bcthlem5  20861  bcth2  20863  bcth3  20864  cmetcusp1OLD  20885  cmetcusp1  20886  cmetcuspOLD  20887  cmetcusp  20888  minveclem3  20938  imsxmet  24105  blocni  24227  ubthlem1  24293  ubthlem2  24294  minvecolem4a  24300  hhxmet  24599  hilxmet  24619  fmcncfil  26383  blssp  28678  lmclim2  28680  geomcau  28681  caures  28682  caushft  28683  sstotbnd2  28699  equivtotbnd  28703  isbndx  28707  isbnd3  28709  ssbnd  28713  totbndbnd  28714  prdstotbnd  28719  prdsbnd2  28720  heibor1lem  28734  heibor1  28735  heiborlem3  28738  heiborlem6  28741  heiborlem8  28743  heiborlem9  28744  heiborlem10  28745  heibor  28746  bfplem1  28747  bfplem2  28748  rrncmslem  28757  ismrer1  28763  reheibor  28764
  Copyright terms: Public domain W3C validator