Theorem ovresd 7505

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 7504	. 2 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴(𝐷 ↾ (𝑋 × 𝑋))𝐵) = (𝐴𝐷𝐵))
4	1, 2, 3	syl2anc 585	1 ⊢ (𝜑 → (𝐴(𝐷 ↾ (𝑋 × 𝑋))𝐵) = (𝐴𝐷𝐵))

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106   × cxp 5622   ↾ cres 5626  (class class class)co 7341

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708  ax-sep 5247  ax-nul 5254  ax-pr 5376

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3444  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4274  df-if 4478  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4857  df-br 5097  df-opab 5159  df-xp 5630  df-res 5636  df-iota 6435  df-fv 6491  df-ov 7344

This theorem is referenced by:  sscres  17632  fullsubc  17662  fullresc  17663  funcres2c  17714  psmetres2  23572  xmetres2  23619  prdsdsf  23625  xpsdsval  23639  xmssym  23723  xmstri2  23724  mstri2  23725  xmstri  23726  mstri  23727  xmstri3  23728  mstri3  23729  msrtri  23730  tmsxpsval  23799  ngptgp  23897  nlmvscn  23956  nrginvrcn  23961  nghmcn  24014  cnmpt1ds  24110  cnmpt2ds  24111  ipcn  24515  caussi  24566  causs  24567  minveclem2  24695  minveclem3b  24697  minveclem3  24698  minveclem4  24701  minveclem6  24703  ftc1lem6  25310  ulmdvlem1  25664  abelth  25705  cxpcn3  26006  rlimcnp  26220  hhssnv  29913  madjusmdetlem3  32075  qqhcn  32237  qqhucn  32238  ftc1cnnc  36005  ismtyres  36122  isdrngo2  36272  naddcnffo  41382  rngchom  45943  ringchom  45989  irinitoringc  46045  rhmsubclem4  46065