Theorem ovresd 7534

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   × cxp 5629   ↾ cres 5633  (class class class)co 7367

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 2708  ax-sep 5231  ax-pr 5375

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 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-xp 5637  df-res 5643  df-iota 6454  df-fv 6506  df-ov 7370

This theorem is referenced by:  sscres  17790  fullsubc  17817  fullresc  17818  funcres2c  17870  rngchom  20600  ringchom  20629  rhmsubclem4  20665  irinitoringc  21459  psmetres2  24279  xmetres2  24326  prdsdsf  24332  xpsdsval  24346  xmssym  24430  xmstri2  24431  mstri2  24432  xmstri  24433  mstri  24434  xmstri3  24435  mstri3  24436  msrtri  24437  tmsxpsval  24503  ngptgp  24601  nlmvscn  24652  nrginvrcn  24657  nghmcn  24710  cnmpt1ds  24808  cnmpt2ds  24809  ipcn  25213  caussi  25264  causs  25265  minveclem2  25393  minveclem3b  25395  minveclem3  25396  minveclem4  25399  minveclem6  25401  ftc1lem6  26008  ulmdvlem1  26365  abelth  26406  cxpcn3  26712  rlimcnp  26929  zsoring  28401  hhssnv  31335  madjusmdetlem3  33973  qqhcn  34135  qqhucn  34136  ftc1cnnc  38013  ismtyres  38129  isdrngo2  38279  naddcnffo  43792