Theorem ovresd 7586

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

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

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 2737  ax-sep 5259  ax-pr 5406

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 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-xp 5669  df-res 5675  df-iota 6496  df-fv 6548  df-ov 7422

This theorem is used by:  sscres  17902  fullsubc  17929  fullresc  17930  funcres2c  17982  mgmn0plusgf  18731  rngchom  20772  ringchom  20801  rhmsubclem4  20837  irinitoringc  21679  psmetres2  24522  xmetres2  24569  prdsdsf  24575  xpsdsval  24589  xmssym  24673  xmstri2  24674  mstri2  24675  xmstri  24676  mstri  24677  xmstri3  24678  mstri3  24679  msrtri  24680  tmsxpsval  24746  ngptgp  24844  nlmvscn  24895  nrginvrcn  24900  nghmcn  24953  cnmpt1ds  25051  cnmpt2ds  25052  ipcn  25456  caussi  25507  causs  25508  minveclem2  25636  minveclem3b  25638  minveclem3  25639  minveclem4  25642  minveclem6  25644  ftc1lem6  26251  ulmdvlem1  26614  abelth  26655  cxpcn3  26964  rlimcnp  27181  zsoring  28653  hhssnv  31687  madjusmdetlem3  34283  qqhcn  34445  qqhucn  34446  ftc1cnnc  38400  ismtyres  38517  isdrngo2  38667  naddcnffo  44149