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

Theorem ovres 6426
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 5031 . . 3  |-  ( ( A  e.  C  /\  B  e.  D )  -> 
<. A ,  B >.  e.  ( C  X.  D
) )
2 fvres 5880 . . 3  |-  ( <. A ,  B >.  e.  ( C  X.  D
)  ->  ( ( F  |`  ( C  X.  D ) ) `  <. A ,  B >. )  =  ( F `  <. A ,  B >. ) )
31, 2syl 16 . 2  |-  ( ( A  e.  C  /\  B  e.  D )  ->  ( ( F  |`  ( C  X.  D
) ) `  <. A ,  B >. )  =  ( F `  <. A ,  B >. ) )
4 df-ov 6287 . 2  |-  ( A ( F  |`  ( C  X.  D ) ) B )  =  ( ( F  |`  ( C  X.  D ) ) `
 <. A ,  B >. )
5 df-ov 6287 . 2  |-  ( A F B )  =  ( F `  <. A ,  B >. )
63, 4, 53eqtr4g 2533 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 369    = wceq 1379    e. wcel 1767   <.cop 4033    X. cxp 4997    |` cres 5001   ` cfv 5588  (class class class)co 6284
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-xp 5005  df-res 5011  df-iota 5551  df-fv 5596  df-ov 6287
This theorem is referenced by:  ovresd  6427  oprssov  6428  ofmresval  6536  cantnfval2  8088  cantnfval2OLD  8118  mulnzcnopr  10195  prdsdsval3  14740  frmdplusg  15854  frmdadd  15855  grpissubg  16026  gaid  16142  gass  16144  gasubg  16145  mplsubrglem  17899  mplsubrglemOLD  17900  mamures  18687  mdetrlin  18899  mdetrsca  18900  pmatcollpw3lem  19079  tsmsxplem1  20418  tsmsxplem2  20419  xmetres2  20627  ressprdsds  20637  blres  20697  xmetresbl  20703  mscl  20727  xmscl  20728  xmsge0  20729  xmseq0  20730  nmfval2  20874  nmval2  20875  isngp3  20881  ngpds  20886  xrsdsre  21078  divcn  21135  cncfmet  21175  cfilresi  21497  cfilres  21498  dvdsmulf1o  23226  subgoov  25011  issubgoi  25016  ablomul  25061  mulid  25062  ghgrplem2  25073  sspgval  25346  sspsval  25348  sspmlem  25349  hhssabloi  25882  hhssnv  25884  hhssmetdval  25898  raddcn  27575  xrge0pluscn  27586  cvmlift2lem9  28424  equivbnd2  29919  ismtyres  29935  iccbnd  29967  exidreslem  29970  divrngcl  29991  isdrngo2  29992
  Copyright terms: Public domain W3C validator