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

Theorem ovres 6442
Description: The value of a restricted operation. (Contributed by FL, 10-Nov-2006.)
Assertion
Ref Expression
ovres

Proof of Theorem ovres
StepHypRef Expression
1 opelxpi 5036 . . 3
2 fvres 5885 . . 3
31, 2syl 16 . 2
4 df-ov 6299 . 2
5 df-ov 6299 . 2
63, 4, 53eqtr4g 2523 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  e.wcel 1818  <.cop 4035  X.cxp 5002  |`cres 5006  `cfv 5593  (class class class)co 6296
This theorem is referenced by:  ovresd  6443  oprssov  6444  ofmresval  6552  cantnfval2  8109  cantnfval2OLD  8139  mulnzcnopr  10220  prdsdsval3  14882  frmdplusg  16022  frmdadd  16023  grpissubg  16221  gaid  16337  gass  16339  gasubg  16340  mplsubrglem  18100  mplsubrglemOLD  18101  mamures  18892  mdetrlin  19104  mdetrsca  19105  pmatcollpw3lem  19284  tsmsxplem1  20655  tsmsxplem2  20656  xmetres2  20864  ressprdsds  20874  blres  20934  xmetresbl  20940  mscl  20964  xmscl  20965  xmsge0  20966  xmseq0  20967  nmfval2  21111  nmval2  21112  isngp3  21118  ngpds  21123  xrsdsre  21315  divcn  21372  cncfmet  21412  cfilresi  21734  cfilres  21735  dvdsmulf1o  23470  subgoov  25307  issubgoi  25312  ablomul  25357  mulid  25358  ghgrplem2OLD  25369  sspgval  25642  sspsval  25644  sspmlem  25645  hhssabloi  26178  hhssnv  26180  hhssmetdval  26194  raddcn  27911  xrge0pluscn  27922  cvmlift2lem9  28756  equivbnd2  30288  ismtyres  30304  iccbnd  30336  exidreslem  30339  divrngcl  30360  isdrngo2  30361  rnghmresel  32772  rnghmsscmap2  32781  rnghmsscmap  32782  rnghmsubcsetclem2  32784  rngcifuestrc  32805  rhmresel  32818  rhmsscmap2  32827  rhmsscmap  32828  rhmsubcsetclem2  32830  rhmsscrnghm  32834  rhmsubcrngclem2  32836  rhmsubclem4  32897
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-xp 5010  df-res 5016  df-iota 5556  df-fv 5601  df-ov 6299
  Copyright terms: Public domain W3C validator