Theorem ovresd 7315

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114   × cxp 5553   ↾ cres 5557  (class class class)co 7156

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-xp 5561  df-res 5567  df-iota 6314  df-fv 6363  df-ov 7159

This theorem is referenced by:  sscres  17093  fullsubc  17120  fullresc  17121  funcres2c  17171  psmetres2  22924  xmetres2  22971  prdsdsf  22977  xpsdsval  22991  xmssym  23075  xmstri2  23076  mstri2  23077  xmstri  23078  mstri  23079  xmstri3  23080  mstri3  23081  msrtri  23082  tmsxpsval  23148  ngptgp  23245  nlmvscn  23296  nrginvrcn  23301  nghmcn  23354  cnmpt1ds  23450  cnmpt2ds  23451  ipcn  23849  caussi  23900  causs  23901  minveclem2  24029  minveclem3b  24031  minveclem3  24032  minveclem4  24035  minveclem6  24037  ftc1lem6  24638  ulmdvlem1  24988  abelth  25029  cxpcn3  25329  rlimcnp  25543  hhssnv  29041  madjusmdetlem3  31094  qqhcn  31232  qqhucn  31233  ftc1cnnc  34981  ismtyres  35101  isdrngo2  35251  rngchom  44258  ringchom  44304  irinitoringc  44360  rhmsubclem4  44380