Theorem ovresd 7525

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113   × cxp 5622   ↾ cres 5626  (class class class)co 7358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-xp 5630  df-res 5636  df-iota 6448  df-fv 6500  df-ov 7361

This theorem is referenced by:  sscres  17747  fullsubc  17774  fullresc  17775  funcres2c  17827  rngchom  20556  ringchom  20585  rhmsubclem4  20621  irinitoringc  21434  psmetres2  24258  xmetres2  24305  prdsdsf  24311  xpsdsval  24325  xmssym  24409  xmstri2  24410  mstri2  24411  xmstri  24412  mstri  24413  xmstri3  24414  mstri3  24415  msrtri  24416  tmsxpsval  24482  ngptgp  24580  nlmvscn  24631  nrginvrcn  24636  nghmcn  24689  cnmpt1ds  24787  cnmpt2ds  24788  ipcn  25202  caussi  25253  causs  25254  minveclem2  25382  minveclem3b  25384  minveclem3  25385  minveclem4  25388  minveclem6  25390  ftc1lem6  26004  ulmdvlem1  26365  abelth  26407  cxpcn3  26714  rlimcnp  26931  zsoring  28405  hhssnv  31339  madjusmdetlem3  33986  qqhcn  34148  qqhucn  34149  ftc1cnnc  37893  ismtyres  38009  isdrngo2  38159  naddcnffo  43606