Theorem ovresd 7617

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108   × cxp 5698   ↾ cres 5702  (class class class)co 7448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-xp 5706  df-res 5712  df-iota 6525  df-fv 6581  df-ov 7451

This theorem is referenced by:  sscres  17884  fullsubc  17914  fullresc  17915  funcres2c  17968  rngchom  20645  ringchom  20674  rhmsubclem4  20710  irinitoringc  21513  psmetres2  24345  xmetres2  24392  prdsdsf  24398  xpsdsval  24412  xmssym  24496  xmstri2  24497  mstri2  24498  xmstri  24499  mstri  24500  xmstri3  24501  mstri3  24502  msrtri  24503  tmsxpsval  24572  ngptgp  24670  nlmvscn  24729  nrginvrcn  24734  nghmcn  24787  cnmpt1ds  24883  cnmpt2ds  24884  ipcn  25299  caussi  25350  causs  25351  minveclem2  25479  minveclem3b  25481  minveclem3  25482  minveclem4  25485  minveclem6  25487  ftc1lem6  26102  ulmdvlem1  26461  abelth  26503  cxpcn3  26809  rlimcnp  27026  hhssnv  31296  madjusmdetlem3  33775  qqhcn  33937  qqhucn  33938  ftc1cnnc  37652  ismtyres  37768  isdrngo2  37918  naddcnffo  43326