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

Theorem ovres 6441
Description: The value of a restricted operation. (Contributed by FL, 10-Nov-2006.)
Assertion
Ref Expression
ovres  |-  ( ( A  e.  C  /\  B  e.  D )  ->  ( A ( F  |`  ( C  X.  D
) ) B )  =  ( A F B ) )

Proof of Theorem ovres
StepHypRef Expression
1 opelxpi 4877 . . 3  |-  ( ( A  e.  C  /\  B  e.  D )  -> 
<. A ,  B >.  e.  ( C  X.  D
) )
2 fvres 5886 . . 3  |-  ( <. A ,  B >.  e.  ( C  X.  D
)  ->  ( ( F  |`  ( C  X.  D ) ) `  <. A ,  B >. )  =  ( F `  <. A ,  B >. ) )
31, 2syl 17 . 2  |-  ( ( A  e.  C  /\  B  e.  D )  ->  ( ( F  |`  ( C  X.  D
) ) `  <. A ,  B >. )  =  ( F `  <. A ,  B >. ) )
4 df-ov 6299 . 2  |-  ( A ( F  |`  ( C  X.  D ) ) B )  =  ( ( F  |`  ( C  X.  D ) ) `
 <. A ,  B >. )
5 df-ov 6299 . 2  |-  ( A F B )  =  ( F `  <. A ,  B >. )
63, 4, 53eqtr4g 2486 1  |-  ( ( A  e.  C  /\  B  e.  D )  ->  ( A ( F  |`  ( C  X.  D
) ) B )  =  ( A F B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437    e. wcel 1867   <.cop 3999    X. cxp 4843    |` cres 4847   ` cfv 5592  (class class class)co 6296
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539  ax-nul 4547  ax-pr 4652
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-rab 2782  df-v 3080  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4214  df-br 4418  df-opab 4476  df-xp 4851  df-res 4857  df-iota 5556  df-fv 5600  df-ov 6299
This theorem is referenced by:  ovresd  6442  oprssov  6443  ofmresval  6549  cantnfval2  8164  mulnzcnopr  10247  prdsdsval3  15335  frmdplusg  16582  frmdadd  16583  grpissubg  16781  gaid  16897  gass  16899  gasubg  16900  mplsubrglem  18591  mamures  19339  mdetrlin  19551  mdetrsca  19552  pmatcollpw3lem  19731  tsmsxplem1  21091  tsmsxplem2  21092  xmetres2  21300  ressprdsds  21310  blres  21370  xmetresbl  21376  mscl  21400  xmscl  21401  xmsge0  21402  xmseq0  21403  nmfval2  21529  nmval2  21530  isngp3  21536  ngpds  21541  xrsdsre  21732  divcn  21789  cncfmet  21829  cfilresi  22151  cfilres  22152  dvdsmulf1o  23983  subgoov  25875  issubgoi  25880  ablomul  25925  mulid  25926  ghgrplem2OLD  25937  sspgval  26210  sspsval  26212  sspmlem  26213  hhssabloi  26745  hhssnv  26747  hhssmetdval  26761  raddcn  28571  xrge0pluscn  28582  cvmlift2lem9  29819  icoreval  31487  icoreelrnab  31488  equivbnd2  31828  ismtyres  31844  iccbnd  31876  exidreslem  31879  divrngcl  31900  isdrngo2  31901  rnghmresel  38737  rnghmsscmap2  38746  rnghmsscmap  38747  rnghmsubcsetclem2  38749  rngcifuestrc  38770  rhmresel  38783  rhmsscmap2  38792  rhmsscmap  38793  rhmsubcsetclem2  38795  rhmsscrnghm  38799  rhmsubcrngclem2  38801  rhmsubclem4  38862
  Copyright terms: Public domain W3C validator