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

Theorem ovresd 6948
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 6947 . 2 ((𝐴𝑋𝐵𝑋) → (𝐴(𝐷 ↾ (𝑋 × 𝑋))𝐵) = (𝐴𝐷𝐵))
41, 2, 3syl2anc 565 1 (𝜑 → (𝐴(𝐷 ↾ (𝑋 × 𝑋))𝐵) = (𝐴𝐷𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1631  wcel 2145   × cxp 5247  cres 5251  (class class class)co 6793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pr 5034
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-xp 5255  df-res 5261  df-iota 5994  df-fv 6039  df-ov 6796
This theorem is referenced by:  sscres  16690  fullsubc  16717  fullresc  16718  funcres2c  16768  psmetres2  22339  xmetres2  22386  prdsdsf  22392  xpsdsval  22406  xmssym  22490  xmstri2  22491  mstri2  22492  xmstri  22493  mstri  22494  xmstri3  22495  mstri3  22496  msrtri  22497  tmsxpsval  22563  ngptgp  22660  nlmvscn  22711  nrginvrcn  22716  nghmcn  22769  cnmpt1ds  22865  cnmpt2ds  22866  ipcn  23264  caussi  23314  causs  23315  minveclem2  23416  minveclem3b  23418  minveclem3  23419  minveclem4  23422  minveclem6  23424  ftc1lem6  24024  ulmdvlem1  24374  abelth  24415  cxpcn3  24710  rlimcnp  24913  hhssnv  28461  madjusmdetlem3  30235  qqhcn  30375  qqhucn  30376  ftc1cnnc  33816  ismtyres  33939  isdrngo2  34089  rngchom  42495  ringchom  42541  irinitoringc  42597  rhmsubclem4  42617
  Copyright terms: Public domain W3C validator