Theorem ovresd 7580

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145   × cxp 5653   ↾ cres 5657  (class class class)co 7413

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-xp 5661  df-res 5667  df-iota 6489  df-fv 6541  df-ov 7416

This theorem is used by:  sscres  17912  fullsubc  17939  fullresc  17940  funcres2c  17992  mgmn0plusgf  18741  rngchom  20785  ringchom  20814  rhmsubclem4  20850  irinitoringc  21692  psmetres2  24540  xmetres2  24587  prdsdsf  24593  xpsdsval  24607  xmssym  24691  xmstri2  24692  mstri2  24693  xmstri  24694  mstri  24695  xmstri3  24696  mstri3  24697  msrtri  24698  tmsxpsval  24764  ngptgp  24862  nlmvscn  24913  nrginvrcn  24918  nghmcn  24971  cnmpt1ds  25069  cnmpt2ds  25070  ipcn  25474  caussi  25525  causs  25526  minveclem2  25654  minveclem3b  25656  minveclem3  25657  minveclem4  25660  minveclem6  25662  ftc1lem6  26268  ulmdvlem1  26636  abelth  26677  cxpcn3  26985  rlimcnp  27202  zsoring  28674  hhssnv  31745  madjusmdetlem3  34339  qqhcn  34501  qqhucn  34502  ftc1cnnc  38441  ismtyres  38558  isdrngo2  38708  naddcnffo  44205