Theorem ovresd 7619

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147   × cxp 5656   ↾ cres 5660  (class class class)co 7451

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-xp 5664  df-res 5670  df-iota 6520  df-fv 6574  df-ov 7454

This theorem is used by:  sscres  18048  fullsubc  18075  fullresc  18076  funcres2c  18128  mgmn0plusgf  18877  rngchom  20926  ringchom  20955  rhmsubclem4  20991  irinitoringc  21840  psmetres2  24688  xmetres2  24735  prdsdsf  24741  xpsdsval  24755  xmssym  24839  xmstri2  24840  mstri2  24841  xmstri  24842  mstri  24843  xmstri3  24844  mstri3  24845  msrtri  24846  tmsxpsval  24912  ngptgp  25010  nlmvscn  25061  nrginvrcn  25066  nghmcn  25119  cnmpt1ds  25217  cnmpt2ds  25218  ipcn  25622  caussi  25673  causs  25674  minveclem2  25802  minveclem3b  25804  minveclem3  25805  minveclem4  25808  minveclem6  25810  ftc1lem6  26416  ulmdvlem1  26784  abelth  26825  cxpcn3  27133  rlimcnp  27350  zsoring  28852  hhssnv  31923  madjusmdetlem3  34572  qqhcn  34734  qqhucn  34735  ftc1cnnc  38878  ismtyres  39008  isdrngo2  39158  naddcnffo  44627