Theorem ovresd 7507

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   × cxp 5611   ↾ cres 5615  (class class class)co 7340

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5231  ax-nul 5241  ax-pr 5367

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3393  df-v 3435  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5089  df-opab 5151  df-xp 5619  df-res 5625  df-iota 6432  df-fv 6484  df-ov 7343

This theorem is referenced by:  sscres  17717  fullsubc  17744  fullresc  17745  funcres2c  17797  rngchom  20492  ringchom  20521  rhmsubclem4  20557  irinitoringc  21370  psmetres2  24183  xmetres2  24230  prdsdsf  24236  xpsdsval  24250  xmssym  24334  xmstri2  24335  mstri2  24336  xmstri  24337  mstri  24338  xmstri3  24339  mstri3  24340  msrtri  24341  tmsxpsval  24407  ngptgp  24505  nlmvscn  24556  nrginvrcn  24561  nghmcn  24614  cnmpt1ds  24712  cnmpt2ds  24713  ipcn  25127  caussi  25178  causs  25179  minveclem2  25307  minveclem3b  25309  minveclem3  25310  minveclem4  25313  minveclem6  25315  ftc1lem6  25929  ulmdvlem1  26290  abelth  26332  cxpcn3  26639  rlimcnp  26856  zsoring  28286  hhssnv  31195  madjusmdetlem3  33810  qqhcn  33972  qqhucn  33973  ftc1cnnc  37689  ismtyres  37805  isdrngo2  37955  naddcnffo  43354