Theorem ovresd 7559

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   × cxp 5639   ↾ cres 5643  (class class class)co 7390

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-xp 5647  df-res 5653  df-iota 6467  df-fv 6522  df-ov 7393

This theorem is referenced by:  sscres  17792  fullsubc  17819  fullresc  17820  funcres2c  17872  rngchom  20539  ringchom  20568  rhmsubclem4  20604  irinitoringc  21396  psmetres2  24209  xmetres2  24256  prdsdsf  24262  xpsdsval  24276  xmssym  24360  xmstri2  24361  mstri2  24362  xmstri  24363  mstri  24364  xmstri3  24365  mstri3  24366  msrtri  24367  tmsxpsval  24433  ngptgp  24531  nlmvscn  24582  nrginvrcn  24587  nghmcn  24640  cnmpt1ds  24738  cnmpt2ds  24739  ipcn  25153  caussi  25204  causs  25205  minveclem2  25333  minveclem3b  25335  minveclem3  25336  minveclem4  25339  minveclem6  25341  ftc1lem6  25955  ulmdvlem1  26316  abelth  26358  cxpcn3  26665  rlimcnp  26882  hhssnv  31200  madjusmdetlem3  33826  qqhcn  33988  qqhucn  33989  ftc1cnnc  37693  ismtyres  37809  isdrngo2  37959  naddcnffo  43360