Theorem ovresd 7556

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   × cxp 5636   ↾ cres 5640  (class class class)co 7387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-xp 5644  df-res 5650  df-iota 6464  df-fv 6519  df-ov 7390

This theorem is referenced by:  sscres  17785  fullsubc  17812  fullresc  17813  funcres2c  17865  rngchom  20532  ringchom  20561  rhmsubclem4  20597  irinitoringc  21389  psmetres2  24202  xmetres2  24249  prdsdsf  24255  xpsdsval  24269  xmssym  24353  xmstri2  24354  mstri2  24355  xmstri  24356  mstri  24357  xmstri3  24358  mstri3  24359  msrtri  24360  tmsxpsval  24426  ngptgp  24524  nlmvscn  24575  nrginvrcn  24580  nghmcn  24633  cnmpt1ds  24731  cnmpt2ds  24732  ipcn  25146  caussi  25197  causs  25198  minveclem2  25326  minveclem3b  25328  minveclem3  25329  minveclem4  25332  minveclem6  25334  ftc1lem6  25948  ulmdvlem1  26309  abelth  26351  cxpcn3  26658  rlimcnp  26875  hhssnv  31193  madjusmdetlem3  33819  qqhcn  33981  qqhucn  33982  ftc1cnnc  37686  ismtyres  37802  isdrngo2  37952  naddcnffo  43353