Theorem ovresd 7563

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

Syntax hints:   → wi 4   = wceq 1560   ∈ wcel 2142   × cxp 5645   ↾ cres 5649  (class class class)co 7396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-xp 5653  df-res 5659  df-iota 6477  df-fv 6529  df-ov 7399

This theorem is referenced by:  sscres  17856  fullsubc  17883  fullresc  17884  funcres2c  17936  rngchom  20669  ringchom  20698  rhmsubclem4  20734  irinitoringc  21528  psmetres2  24371  xmetres2  24418  prdsdsf  24424  xpsdsval  24438  xmssym  24522  xmstri2  24523  mstri2  24524  xmstri  24525  mstri  24526  xmstri3  24527  mstri3  24528  msrtri  24529  tmsxpsval  24595  ngptgp  24693  nlmvscn  24744  nrginvrcn  24749  nghmcn  24802  cnmpt1ds  24900  cnmpt2ds  24901  ipcn  25305  caussi  25356  causs  25357  minveclem2  25485  minveclem3b  25487  minveclem3  25488  minveclem4  25491  minveclem6  25493  ftc1lem6  26100  ulmdvlem1  26460  abelth  26501  cxpcn3  26810  rlimcnp  27027  zsoring  28499  hhssnv  31464  madjusmdetlem3  34123  qqhcn  34285  qqhucn  34286  ftc1cnnc  38188  ismtyres  38304  isdrngo2  38454  naddcnffo  43938