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

Theorem ovresd 7299
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 7298 . 2 ((𝐴𝑋𝐵𝑋) → (𝐴(𝐷 ↾ (𝑋 × 𝑋))𝐵) = (𝐴𝐷𝐵))
41, 2, 3syl2anc 587 1 (𝜑 → (𝐴(𝐷 ↾ (𝑋 × 𝑋))𝐵) = (𝐴𝐷𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2112   × cxp 5521  cres 5525  (class class class)co 7139
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pr 5298
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rex 3115  df-v 3446  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-xp 5529  df-res 5535  df-iota 6287  df-fv 6336  df-ov 7142
This theorem is referenced by:  sscres  17089  fullsubc  17116  fullresc  17117  funcres2c  17167  psmetres2  22925  xmetres2  22972  prdsdsf  22978  xpsdsval  22992  xmssym  23076  xmstri2  23077  mstri2  23078  xmstri  23079  mstri  23080  xmstri3  23081  mstri3  23082  msrtri  23083  tmsxpsval  23149  ngptgp  23246  nlmvscn  23297  nrginvrcn  23302  nghmcn  23355  cnmpt1ds  23451  cnmpt2ds  23452  ipcn  23854  caussi  23905  causs  23906  minveclem2  24034  minveclem3b  24036  minveclem3  24037  minveclem4  24040  minveclem6  24042  ftc1lem6  24648  ulmdvlem1  24999  abelth  25040  cxpcn3  25341  rlimcnp  25555  hhssnv  29051  madjusmdetlem3  31186  qqhcn  31346  qqhucn  31347  ftc1cnnc  35128  ismtyres  35245  isdrngo2  35395  rngchom  44584  ringchom  44630  irinitoringc  44686  rhmsubclem4  44706
  Copyright terms: Public domain W3C validator