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

Theorem ovresd 6757
 Description: Lemma for converting metric theorems to metric space theorems. (Contributed by Mario Carneiro, 2-Oct-2015.)
Hypotheses
Ref Expression
ovresd.1 (𝜑𝐴𝑋)
ovresd.2 (𝜑𝐵𝑋)
Assertion
Ref Expression
ovresd (𝜑 → (𝐴(𝐷 ↾ (𝑋 × 𝑋))𝐵) = (𝐴𝐷𝐵))

Proof of Theorem ovresd
StepHypRef Expression
1 ovresd.1 . 2 (𝜑𝐴𝑋)
2 ovresd.2 . 2 (𝜑𝐵𝑋)
3 ovres 6756 . 2 ((𝐴𝑋𝐵𝑋) → (𝐴(𝐷 ↾ (𝑋 × 𝑋))𝐵) = (𝐴𝐷𝐵))
41, 2, 3syl2anc 692 1 (𝜑 → (𝐴(𝐷 ↾ (𝑋 × 𝑋))𝐵) = (𝐴𝐷𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1480   ∈ wcel 1987   × cxp 5074   ↾ cres 5078  (class class class)co 6607 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4743  ax-nul 4751  ax-pr 4869 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-nul 3894  df-if 4061  df-sn 4151  df-pr 4153  df-op 4157  df-uni 4405  df-br 4616  df-opab 4676  df-xp 5082  df-res 5088  df-iota 5812  df-fv 5857  df-ov 6610 This theorem is referenced by:  sscres  16407  fullsubc  16434  fullresc  16435  funcres2c  16485  psmetres2  22032  xmetres2  22079  prdsdsf  22085  xpsdsval  22099  xmssym  22183  xmstri2  22184  mstri2  22185  xmstri  22186  mstri  22187  xmstri3  22188  mstri3  22189  msrtri  22190  tmsxpsval  22256  ngptgp  22353  nlmvscn  22404  nrginvrcn  22409  nghmcn  22462  cnmpt1ds  22558  cnmpt2ds  22559  ipcn  22958  caussi  23008  causs  23009  minveclem2  23110  minveclem3b  23112  minveclem3  23113  minveclem4  23116  minveclem6  23118  ftc1lem6  23715  ulmdvlem1  24065  abelth  24106  cxpcn3  24396  rlimcnp  24599  hhssnv  27982  madjusmdetlem3  29689  qqhcn  29829  qqhucn  29830  ftc1cnnc  33137  ismtyres  33260  isdrngo2  33410  rngchom  41271  ringchom  41317  irinitoringc  41373  rhmsubclem4  41393
 Copyright terms: Public domain W3C validator