Theorem ovresd 7578

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

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149   × cxp 5660   ↾ cres 5664  (class class class)co 7411

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-xp 5668  df-res 5674  df-iota 6493  df-fv 6545  df-ov 7414

This theorem is referenced by:  sscres  17879  fullsubc  17906  fullresc  17907  funcres2c  17959  rngchom  20707  ringchom  20736  rhmsubclem4  20772  irinitoringc  21597  psmetres2  24439  xmetres2  24486  prdsdsf  24492  xpsdsval  24506  xmssym  24590  xmstri2  24591  mstri2  24592  xmstri  24593  mstri  24594  xmstri3  24595  mstri3  24596  msrtri  24597  tmsxpsval  24663  ngptgp  24761  nlmvscn  24812  nrginvrcn  24817  nghmcn  24870  cnmpt1ds  24968  cnmpt2ds  24969  ipcn  25373  caussi  25424  causs  25425  minveclem2  25553  minveclem3b  25555  minveclem3  25556  minveclem4  25559  minveclem6  25561  ftc1lem6  26168  ulmdvlem1  26528  abelth  26569  cxpcn3  26878  rlimcnp  27095  zsoring  28567  hhssnv  31556  madjusmdetlem3  34163  qqhcn  34325  qqhucn  34326  ftc1cnnc  38230  ismtyres  38346  isdrngo2  38496  naddcnffo  43982