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

Theorem ovres 6229
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 4867 . . 3  |-  ( ( A  e.  C  /\  B  e.  D )  -> 
<. A ,  B >.  e.  ( C  X.  D
) )
2 fvres 5701 . . 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 6093 . 2  |-  ( A ( F  |`  ( C  X.  D ) ) B )  =  ( ( F  |`  ( C  X.  D ) ) `
 <. A ,  B >. )
5 df-ov 6093 . 2  |-  ( A F B )  =  ( F `  <. A ,  B >. )
63, 4, 53eqtr4g 2498 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 1364    e. wcel 1761   <.cop 3880    X. cxp 4834    |` cres 4838   ` cfv 5415  (class class class)co 6090
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pr 4528
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-br 4290  df-opab 4348  df-xp 4842  df-res 4848  df-iota 5378  df-fv 5423  df-ov 6093
This theorem is referenced by:  ovresd  6230  oprssov  6231  ofmresval  6331  cantnfval2  7873  cantnfval2OLD  7903  mulnzcnopr  9978  prdsdsval3  14419  frmdplusg  15525  frmdadd  15526  grpissubg  15694  gaid  15810  gass  15812  gasubg  15813  mplsubrglem  17507  mplsubrglemOLD  17508  mamures  18190  mdetrlin  18309  mdetrsca  18310  tsmsxplem1  19627  tsmsxplem2  19628  xmetres2  19836  ressprdsds  19846  blres  19906  xmetresbl  19912  mscl  19936  xmscl  19937  xmsge0  19938  xmseq0  19939  nmfval2  20083  nmval2  20084  isngp3  20090  ngpds  20095  xrsdsre  20287  divcn  20344  cncfmet  20384  cfilresi  20706  cfilres  20707  dvdsmulf1o  22477  subgoov  23711  issubgoi  23716  ablomul  23761  mulid  23762  ghgrplem2  23773  sspgval  24046  sspsval  24048  sspmlem  24049  hhssabloi  24582  hhssnv  24584  hhssmetdval  24598  raddcn  26279  xrge0pluscn  26290  cvmlift2lem9  27114  equivbnd2  28600  ismtyres  28616  iccbnd  28648  exidreslem  28651  divrngcl  28672  isdrngo2  28673
  Copyright terms: Public domain W3C validator