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

Theorem ovres 6230
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 4871 . . 3  |-  ( ( A  e.  C  /\  B  e.  D )  -> 
<. A ,  B >.  e.  ( C  X.  D
) )
2 fvres 5704 . . 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 6094 . 2  |-  ( A ( F  |`  ( C  X.  D ) ) B )  =  ( ( F  |`  ( C  X.  D ) ) `
 <. A ,  B >. )
5 df-ov 6094 . 2  |-  ( A F B )  =  ( F `  <. A ,  B >. )
63, 4, 53eqtr4g 2500 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 1369    e. wcel 1756   <.cop 3883    X. cxp 4838    |` cres 4842   ` cfv 5418  (class class class)co 6091
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4413  ax-nul 4421  ax-pr 4531
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-br 4293  df-opab 4351  df-xp 4846  df-res 4852  df-iota 5381  df-fv 5426  df-ov 6094
This theorem is referenced by:  ovresd  6231  oprssov  6232  ofmresval  6332  cantnfval2  7877  cantnfval2OLD  7907  mulnzcnopr  9982  prdsdsval3  14423  frmdplusg  15532  frmdadd  15533  grpissubg  15701  gaid  15817  gass  15819  gasubg  15820  mplsubrglem  17517  mplsubrglemOLD  17518  mamures  18290  mdetrlin  18409  mdetrsca  18410  tsmsxplem1  19727  tsmsxplem2  19728  xmetres2  19936  ressprdsds  19946  blres  20006  xmetresbl  20012  mscl  20036  xmscl  20037  xmsge0  20038  xmseq0  20039  nmfval2  20183  nmval2  20184  isngp3  20190  ngpds  20195  xrsdsre  20387  divcn  20444  cncfmet  20484  cfilresi  20806  cfilres  20807  dvdsmulf1o  22534  subgoov  23792  issubgoi  23797  ablomul  23842  mulid  23843  ghgrplem2  23854  sspgval  24127  sspsval  24129  sspmlem  24130  hhssabloi  24663  hhssnv  24665  hhssmetdval  24679  raddcn  26359  xrge0pluscn  26370  cvmlift2lem9  27200  equivbnd2  28691  ismtyres  28707  iccbnd  28739  exidreslem  28742  divrngcl  28763  isdrngo2  28764
  Copyright terms: Public domain W3C validator