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

Theorem ovresd 7526
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 7525 . 2 ((𝐴𝑋𝐵𝑋) → (𝐴(𝐷 ↾ (𝑋 × 𝑋))𝐵) = (𝐴𝐷𝐵))
41, 2, 3syl2anc 585 1 (𝜑 → (𝐴(𝐷 ↾ (𝑋 × 𝑋))𝐵) = (𝐴𝐷𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2107   × cxp 5636  cres 5640  (class class class)co 7362
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pr 5389
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066  df-rex 3075  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-xp 5644  df-res 5650  df-iota 6453  df-fv 6509  df-ov 7365
This theorem is referenced by:  sscres  17713  fullsubc  17743  fullresc  17744  funcres2c  17795  psmetres2  23683  xmetres2  23730  prdsdsf  23736  xpsdsval  23750  xmssym  23834  xmstri2  23835  mstri2  23836  xmstri  23837  mstri  23838  xmstri3  23839  mstri3  23840  msrtri  23841  tmsxpsval  23910  ngptgp  24008  nlmvscn  24067  nrginvrcn  24072  nghmcn  24125  cnmpt1ds  24221  cnmpt2ds  24222  ipcn  24626  caussi  24677  causs  24678  minveclem2  24806  minveclem3b  24808  minveclem3  24809  minveclem4  24812  minveclem6  24814  ftc1lem6  25421  ulmdvlem1  25775  abelth  25816  cxpcn3  26117  rlimcnp  26331  hhssnv  30248  madjusmdetlem3  32450  qqhcn  32612  qqhucn  32613  ftc1cnnc  36179  ismtyres  36296  isdrngo2  36446  naddcnffo  41709  rngchom  46339  ringchom  46385  irinitoringc  46441  rhmsubclem4  46461
  Copyright terms: Public domain W3C validator