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

Theorem ovres 5987
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 4721 . . 3  |-  ( ( A  e.  C  /\  B  e.  D )  -> 
<. A ,  B >.  e.  ( C  X.  D
) )
2 fvres 5542 . . 3  |-  ( <. A ,  B >.  e.  ( C  X.  D
)  ->  ( ( F  |`  ( C  X.  D ) ) `  <. A ,  B >. )  =  ( F `  <. A ,  B >. ) )
31, 2syl 15 . 2  |-  ( ( A  e.  C  /\  B  e.  D )  ->  ( ( F  |`  ( C  X.  D
) ) `  <. A ,  B >. )  =  ( F `  <. A ,  B >. ) )
4 df-ov 5861 . 2  |-  ( A ( F  |`  ( C  X.  D ) ) B )  =  ( ( F  |`  ( C  X.  D ) ) `
 <. A ,  B >. )
5 df-ov 5861 . 2  |-  ( A F B )  =  ( F `  <. A ,  B >. )
63, 4, 53eqtr4g 2340 1  |-  ( ( A  e.  C  /\  B  e.  D )  ->  ( A ( F  |`  ( C  X.  D
) ) B )  =  ( A F B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1623    e. wcel 1684   <.cop 3643    X. cxp 4687    |` cres 4691   ` cfv 5255  (class class class)co 5858
This theorem is referenced by:  ovresd  5988  oprssov  5989  ofmresval  6117  cantnfval2  7370  mulnzcnopr  9414  prdsdsval3  13384  frmdplusg  14476  frmdadd  14477  gaid  14753  gass  14755  gasubg  14756  mplsubrglem  16183  tsmsxplem1  17835  tsmsxplem2  17836  xmetres2  17925  prdsdsf  17931  ressprdsds  17935  xpsdsval  17945  blres  17977  xmetresbl  17983  mscl  18007  xmscl  18008  xmsge0  18009  xmseq0  18010  nmfval2  18113  nmval2  18114  isngp3  18120  ngpds  18125  xrsdsre  18316  divcn  18372  cncfmet  18412  cfilresi  18721  cfilres  18722  dvdsmulf1o  20434  subgoov  20972  issubgoi  20977  ablomul  21022  mulid  21023  ghgrplem2  21034  sspgval  21305  sspsval  21307  sspmlem  21308  hhssabloi  21839  hhssnv  21841  hhssmetdval  21855  xrge0pluscn  23322  cvmlift2lem9  23842  nZdef  25180  equivbnd2  26516  ismtyres  26532  iccbnd  26564  exidreslem  26567  divrngcl  26588  isdrngo2  26589
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-xp 4695  df-res 4701  df-iota 5219  df-fv 5263  df-ov 5861
  Copyright terms: Public domain W3C validator