Theorem ovresd 7590

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146   × cxp 5664   ↾ cres 5668  (class class class)co 7423

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-xp 5672  df-res 5678  df-iota 6499  df-fv 6551  df-ov 7426

This theorem is used by:  sscres  17905  fullsubc  17932  fullresc  17933  funcres2c  17985  rngchom  20752  ringchom  20781  rhmsubclem4  20817  irinitoringc  21659  psmetres2  24501  xmetres2  24548  prdsdsf  24554  xpsdsval  24568  xmssym  24652  xmstri2  24653  mstri2  24654  xmstri  24655  mstri  24656  xmstri3  24657  mstri3  24658  msrtri  24659  tmsxpsval  24725  ngptgp  24823  nlmvscn  24874  nrginvrcn  24879  nghmcn  24932  cnmpt1ds  25030  cnmpt2ds  25031  ipcn  25435  caussi  25486  causs  25487  minveclem2  25615  minveclem3b  25617  minveclem3  25618  minveclem4  25621  minveclem6  25623  ftc1lem6  26230  ulmdvlem1  26593  abelth  26634  cxpcn3  26943  rlimcnp  27160  zsoring  28632  hhssnv  31646  madjusmdetlem3  34243  qqhcn  34405  qqhucn  34406  ftc1cnnc  38376  ismtyres  38492  isdrngo2  38642  naddcnffo  44124