Theorem ovresd 7523

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

Step	Hyp	Ref	Expression
1		ovresd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝑋)
2		ovresd.2	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝑋)
3		ovres 7522	. 2 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴(𝐷 ↾ (𝑋 × 𝑋))𝐵) = (𝐴𝐷𝐵))
4	1, 2, 3	syl2anc 590	1 ⊢ (𝜑 → (𝐴(𝐷 ↾ (𝑋 × 𝑋))𝐵) = (𝐴𝐷𝐵))

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119   × cxp 5616   ↾ cres 5620  (class class class)co 7356

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-xp 5624  df-res 5630  df-iota 6441  df-fv 6493  df-ov 7359

This theorem is referenced by:  sscres  17781  fullsubc  17808  fullresc  17809  funcres2c  17861  rngchom  20595  ringchom  20624  rhmsubclem4  20660  irinitoringc  21454  psmetres2  24297  xmetres2  24344  prdsdsf  24350  xpsdsval  24364  xmssym  24448  xmstri2  24449  mstri2  24450  xmstri  24451  mstri  24452  xmstri3  24453  mstri3  24454  msrtri  24455  tmsxpsval  24521  ngptgp  24619  nlmvscn  24670  nrginvrcn  24675  nghmcn  24728  cnmpt1ds  24826  cnmpt2ds  24827  ipcn  25231  caussi  25282  causs  25283  minveclem2  25411  minveclem3b  25413  minveclem3  25414  minveclem4  25417  minveclem6  25419  ftc1lem6  26026  ulmdvlem1  26383  abelth  26424  cxpcn3  26730  rlimcnp  26947  zsoring  28419  hhssnv  31353  madjusmdetlem3  34013  qqhcn  34175  qqhucn  34176  ftc1cnnc  38059  ismtyres  38175  isdrngo2  38325  naddcnffo  43809