Theorem ovresd 7162

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

Syntax hints:   → wi 4   = wceq 1520   ∈ wcel 2079   × cxp 5433   ↾ cres 5437  (class class class)co 7007

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-ext 2767  ax-sep 5088  ax-nul 5095  ax-pr 5214

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1080  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3434  df-dif 3857  df-un 3859  df-in 3861  df-ss 3869  df-nul 4207  df-if 4376  df-sn 4467  df-pr 4469  df-op 4473  df-uni 4740  df-br 4957  df-opab 5019  df-xp 5441  df-res 5447  df-iota 6181  df-fv 6225  df-ov 7010

This theorem is referenced by:  sscres  16910  fullsubc  16937  fullresc  16938  funcres2c  16988  psmetres2  22595  xmetres2  22642  prdsdsf  22648  xpsdsval  22662  xmssym  22746  xmstri2  22747  mstri2  22748  xmstri  22749  mstri  22750  xmstri3  22751  mstri3  22752  msrtri  22753  tmsxpsval  22819  ngptgp  22916  nlmvscn  22967  nrginvrcn  22972  nghmcn  23025  cnmpt1ds  23121  cnmpt2ds  23122  ipcn  23520  caussi  23571  causs  23572  minveclem2  23700  minveclem3b  23702  minveclem3  23703  minveclem4  23706  minveclem6  23708  ftc1lem6  24309  ulmdvlem1  24659  abelth  24700  cxpcn3  24998  rlimcnp  25213  hhssnv  28720  madjusmdetlem3  30665  qqhcn  30805  qqhucn  30806  ftc1cnnc  34443  ismtyres  34564  isdrngo2  34714  rngchom  43670  ringchom  43716  irinitoringc  43772  rhmsubclem4  43792