Theorem ovresd 7535

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   × cxp 5630   ↾ cres 5634  (class class class)co 7368

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-xp 5638  df-res 5644  df-iota 6456  df-fv 6508  df-ov 7371

This theorem is referenced by:  sscres  17759  fullsubc  17786  fullresc  17787  funcres2c  17839  rngchom  20568  ringchom  20597  rhmsubclem4  20633  irinitoringc  21446  psmetres2  24270  xmetres2  24317  prdsdsf  24323  xpsdsval  24337  xmssym  24421  xmstri2  24422  mstri2  24423  xmstri  24424  mstri  24425  xmstri3  24426  mstri3  24427  msrtri  24428  tmsxpsval  24494  ngptgp  24592  nlmvscn  24643  nrginvrcn  24648  nghmcn  24701  cnmpt1ds  24799  cnmpt2ds  24800  ipcn  25214  caussi  25265  causs  25266  minveclem2  25394  minveclem3b  25396  minveclem3  25397  minveclem4  25400  minveclem6  25402  ftc1lem6  26016  ulmdvlem1  26377  abelth  26419  cxpcn3  26726  rlimcnp  26943  zsoring  28417  hhssnv  31352  madjusmdetlem3  34007  qqhcn  34169  qqhucn  34170  ftc1cnnc  37943  ismtyres  38059  isdrngo2  38209  naddcnffo  43721