Theorem ovresd 7353

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

Syntax hints:   → wi 4   = wceq 1543   ∈ wcel 2112   × cxp 5534   ↾ cres 5538  (class class class)co 7191

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-opab 5102  df-xp 5542  df-res 5548  df-iota 6316  df-fv 6366  df-ov 7194

This theorem is referenced by:  sscres  17282  fullsubc  17310  fullresc  17311  funcres2c  17362  psmetres2  23166  xmetres2  23213  prdsdsf  23219  xpsdsval  23233  xmssym  23317  xmstri2  23318  mstri2  23319  xmstri  23320  mstri  23321  xmstri3  23322  mstri3  23323  msrtri  23324  tmsxpsval  23390  ngptgp  23488  nlmvscn  23539  nrginvrcn  23544  nghmcn  23597  cnmpt1ds  23693  cnmpt2ds  23694  ipcn  24097  caussi  24148  causs  24149  minveclem2  24277  minveclem3b  24279  minveclem3  24280  minveclem4  24283  minveclem6  24285  ftc1lem6  24892  ulmdvlem1  25246  abelth  25287  cxpcn3  25588  rlimcnp  25802  hhssnv  29299  madjusmdetlem3  31447  qqhcn  31607  qqhucn  31608  ftc1cnnc  35535  ismtyres  35652  isdrngo2  35802  rngchom  45141  ringchom  45187  irinitoringc  45243  rhmsubclem4  45263