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 584	1 ⊢ (𝜑 → (𝐴(𝐷 ↾ (𝑋 × 𝑋))𝐵) = (𝐴𝐷𝐵))

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113   × cxp 5620   ↾ cres 5624  (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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-xp 5628  df-res 5634  df-iota 6446  df-fv 6498  df-ov 7359

This theorem is referenced by:  sscres  17745  fullsubc  17772  fullresc  17773  funcres2c  17825  rngchom  20554  ringchom  20583  rhmsubclem4  20619  irinitoringc  21432  psmetres2  24256  xmetres2  24303  prdsdsf  24309  xpsdsval  24323  xmssym  24407  xmstri2  24408  mstri2  24409  xmstri  24410  mstri  24411  xmstri3  24412  mstri3  24413  msrtri  24414  tmsxpsval  24480  ngptgp  24578  nlmvscn  24629  nrginvrcn  24634  nghmcn  24687  cnmpt1ds  24785  cnmpt2ds  24786  ipcn  25200  caussi  25251  causs  25252  minveclem2  25380  minveclem3b  25382  minveclem3  25383  minveclem4  25386  minveclem6  25388  ftc1lem6  26002  ulmdvlem1  26363  abelth  26405  cxpcn3  26712  rlimcnp  26929  zsoring  28367  hhssnv  31288  madjusmdetlem3  33935  qqhcn  34097  qqhucn  34098  ftc1cnnc  37832  ismtyres  37948  isdrngo2  38098  naddcnffo  43548