Theorem ovresd 7572

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108   × cxp 5652   ↾ cres 5656  (class class class)co 7403

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-xp 5660  df-res 5666  df-iota 6483  df-fv 6538  df-ov 7406

This theorem is referenced by:  sscres  17834  fullsubc  17861  fullresc  17862  funcres2c  17914  rngchom  20581  ringchom  20610  rhmsubclem4  20646  irinitoringc  21438  psmetres2  24251  xmetres2  24298  prdsdsf  24304  xpsdsval  24318  xmssym  24402  xmstri2  24403  mstri2  24404  xmstri  24405  mstri  24406  xmstri3  24407  mstri3  24408  msrtri  24409  tmsxpsval  24475  ngptgp  24573  nlmvscn  24624  nrginvrcn  24629  nghmcn  24682  cnmpt1ds  24780  cnmpt2ds  24781  ipcn  25196  caussi  25247  causs  25248  minveclem2  25376  minveclem3b  25378  minveclem3  25379  minveclem4  25382  minveclem6  25384  ftc1lem6  25998  ulmdvlem1  26359  abelth  26401  cxpcn3  26708  rlimcnp  26925  hhssnv  31191  madjusmdetlem3  33806  qqhcn  33968  qqhucn  33969  ftc1cnnc  37662  ismtyres  37778  isdrngo2  37928  naddcnffo  43335