MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ovres Structured version   Visualization version   GIF version

Theorem ovres 7298
Description: The value of a restricted operation. (Contributed by FL, 10-Nov-2006.)
Assertion
Ref Expression
ovres ((𝐴𝐶𝐵𝐷) → (𝐴(𝐹 ↾ (𝐶 × 𝐷))𝐵) = (𝐴𝐹𝐵))

Proof of Theorem ovres
StepHypRef Expression
1 opelxpi 5560 . . 3 ((𝐴𝐶𝐵𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷))
21fvresd 6669 . 2 ((𝐴𝐶𝐵𝐷) → ((𝐹 ↾ (𝐶 × 𝐷))‘⟨𝐴, 𝐵⟩) = (𝐹‘⟨𝐴, 𝐵⟩))
3 df-ov 7142 . 2 (𝐴(𝐹 ↾ (𝐶 × 𝐷))𝐵) = ((𝐹 ↾ (𝐶 × 𝐷))‘⟨𝐴, 𝐵⟩)
4 df-ov 7142 . 2 (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
52, 3, 43eqtr4g 2861 1 ((𝐴𝐶𝐵𝐷) → (𝐴(𝐹 ↾ (𝐶 × 𝐷))𝐵) = (𝐴𝐹𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538  wcel 2112  cop 4534   × cxp 5521  cres 5525  cfv 6328  (class class class)co 7139
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pr 5298
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rex 3115  df-v 3446  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-xp 5529  df-res 5535  df-iota 6287  df-fv 6336  df-ov 7142
This theorem is referenced by:  ovresd  7299  oprres  7300  oprssov  7301  ofmresval  7406  cantnfval2  9120  mulnzcnopr  11279  prdsdsval3  16753  mgmsscl  17852  frmdplusg  18014  frmdadd  18015  grpissubg  18294  gaid  18424  gass  18426  gasubg  18427  mplsubrglem  20680  mamures  21000  mdetrlin  21210  mdetrsca  21211  pmatcollpw3lem  21391  tsmsxplem1  22761  tsmsxplem2  22762  xmetres2  22971  ressprdsds  22981  blres  23041  xmetresbl  23047  mscl  23071  xmscl  23072  xmsge0  23073  xmseq0  23074  nmfval2  23200  nmval2  23201  isngp3  23207  ngpds  23213  ngpocelbl  23313  xrsdsre  23418  divcn  23476  cncfmet  23517  cfilresi  23902  cfilres  23903  dvdsmulf1o  25782  sspgval  28515  sspsval  28517  sspmlem  28518  hhssabloilem  29047  hhssabloi  29048  hhssnv  29050  hhssmetdval  29063  raddcn  31280  xrge0pluscn  31291  cvmlift2lem9  32666  icoreval  34765  icoreelrnab  34766  equivbnd2  35223  ismtyres  35239  iccbnd  35271  exidreslem  35308  divrngcl  35388  isdrngo2  35389  rnghmresel  44575  rnghmsscmap2  44584  rnghmsscmap  44585  rnghmsubcsetclem2  44587  rngcifuestrc  44608  rhmresel  44621  rhmsscmap2  44630  rhmsscmap  44631  rhmsubcsetclem2  44633  rhmsscrnghm  44637  rhmsubcrngclem2  44639  rhmsubclem4  44700
  Copyright terms: Public domain W3C validator