Theorem ovresd 7536

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   × cxp 5629   ↾ cres 5633  (class class class)co 7369

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 5246  ax-nul 5256  ax-pr 5382

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-xp 5637  df-res 5643  df-iota 6452  df-fv 6507  df-ov 7372

This theorem is referenced by:  sscres  17761  fullsubc  17788  fullresc  17789  funcres2c  17841  rngchom  20508  ringchom  20537  rhmsubclem4  20573  irinitoringc  21365  psmetres2  24178  xmetres2  24225  prdsdsf  24231  xpsdsval  24245  xmssym  24329  xmstri2  24330  mstri2  24331  xmstri  24332  mstri  24333  xmstri3  24334  mstri3  24335  msrtri  24336  tmsxpsval  24402  ngptgp  24500  nlmvscn  24551  nrginvrcn  24556  nghmcn  24609  cnmpt1ds  24707  cnmpt2ds  24708  ipcn  25122  caussi  25173  causs  25174  minveclem2  25302  minveclem3b  25304  minveclem3  25305  minveclem4  25308  minveclem6  25310  ftc1lem6  25924  ulmdvlem1  26285  abelth  26327  cxpcn3  26634  rlimcnp  26851  hhssnv  31166  madjusmdetlem3  33792  qqhcn  33954  qqhucn  33955  ftc1cnnc  37659  ismtyres  37775  isdrngo2  37925  naddcnffo  43326