Theorem ovresd 7585

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

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

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 2733  ax-sep 5249  ax-pr 5391

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 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 5657  df-res 5663  df-iota 6493  df-fv 6545  df-ov 7421

This theorem is used by:  sscres  17991  fullsubc  18018  fullresc  18019  funcres2c  18071  mgmn0plusgf  18820  rngchom  20868  ringchom  20897  rhmsubclem4  20933  irinitoringc  21778  psmetres2  24626  xmetres2  24673  prdsdsf  24679  xpsdsval  24693  xmssym  24777  xmstri2  24778  mstri2  24779  xmstri  24780  mstri  24781  xmstri3  24782  mstri3  24783  msrtri  24784  tmsxpsval  24850  ngptgp  24948  nlmvscn  24999  nrginvrcn  25004  nghmcn  25057  cnmpt1ds  25155  cnmpt2ds  25156  ipcn  25560  caussi  25611  causs  25612  minveclem2  25740  minveclem3b  25742  minveclem3  25743  minveclem4  25746  minveclem6  25748  ftc1lem6  26354  ulmdvlem1  26720  abelth  26761  cxpcn3  27069  rlimcnp  27286  zsoring  28788  hhssnv  31859  madjusmdetlem3  34454  qqhcn  34616  qqhucn  34617  ftc1cnnc  38590  ismtyres  38722  isdrngo2  38872  naddcnffo  44350