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

Theorem ovres 6415
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 5020 . . 3  |-  ( ( A  e.  C  /\  B  e.  D )  -> 
<. A ,  B >.  e.  ( C  X.  D
) )
2 fvres 5862 . . 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 6273 . 2  |-  ( A ( F  |`  ( C  X.  D ) ) B )  =  ( ( F  |`  ( C  X.  D ) ) `
 <. A ,  B >. )
5 df-ov 6273 . 2  |-  ( A F B )  =  ( F `  <. A ,  B >. )
63, 4, 53eqtr4g 2520 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 367    = wceq 1398    e. wcel 1823   <.cop 4022    X. cxp 4986    |` cres 4990   ` cfv 5570  (class class class)co 6270
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-xp 4994  df-res 5000  df-iota 5534  df-fv 5578  df-ov 6273
This theorem is referenced by:  ovresd  6416  oprssov  6417  ofmresval  6525  cantnfval2  8079  cantnfval2OLD  8109  mulnzcnopr  10191  prdsdsval3  14974  frmdplusg  16221  frmdadd  16222  grpissubg  16420  gaid  16536  gass  16538  gasubg  16539  mplsubrglem  18295  mplsubrglemOLD  18296  mamures  19059  mdetrlin  19271  mdetrsca  19272  pmatcollpw3lem  19451  tsmsxplem1  20821  tsmsxplem2  20822  xmetres2  21030  ressprdsds  21040  blres  21100  xmetresbl  21106  mscl  21130  xmscl  21131  xmsge0  21132  xmseq0  21133  nmfval2  21277  nmval2  21278  isngp3  21284  ngpds  21289  xrsdsre  21481  divcn  21538  cncfmet  21578  cfilresi  21900  cfilres  21901  dvdsmulf1o  23668  subgoov  25505  issubgoi  25510  ablomul  25555  mulid  25556  ghgrplem2OLD  25567  sspgval  25840  sspsval  25842  sspmlem  25843  hhssabloi  26376  hhssnv  26378  hhssmetdval  26392  raddcn  28146  xrge0pluscn  28157  cvmlift2lem9  29020  equivbnd2  30528  ismtyres  30544  iccbnd  30576  exidreslem  30579  divrngcl  30600  isdrngo2  30601  rnghmresel  33026  rnghmsscmap2  33035  rnghmsscmap  33036  rnghmsubcsetclem2  33038  rngcifuestrc  33059  rhmresel  33072  rhmsscmap2  33081  rhmsscmap  33082  rhmsubcsetclem2  33084  rhmsscrnghm  33088  rhmsubcrngclem2  33090  rhmsubclem4  33151
  Copyright terms: Public domain W3C validator