Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ovmpod Structured version   Visualization version   GIF version

Theorem ovmpod 7292
 Description: Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 7-Dec-2014.)
Hypotheses
Ref Expression
ovmpod.1 (𝜑𝐹 = (𝑥𝐶, 𝑦𝐷𝑅))
ovmpod.2 ((𝜑 ∧ (𝑥 = 𝐴𝑦 = 𝐵)) → 𝑅 = 𝑆)
ovmpod.3 (𝜑𝐴𝐶)
ovmpod.4 (𝜑𝐵𝐷)
ovmpod.5 (𝜑𝑆𝑋)
Assertion
Ref Expression
ovmpod (𝜑 → (𝐴𝐹𝐵) = 𝑆)
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝑆,𝑦   𝜑,𝑥,𝑦
Allowed substitution hints:   𝐶(𝑥,𝑦)   𝐷(𝑥,𝑦)   𝑅(𝑥,𝑦)   𝐹(𝑥,𝑦)   𝑋(𝑥,𝑦)

Proof of Theorem ovmpod
StepHypRef Expression
1 ovmpod.1 . 2 (𝜑𝐹 = (𝑥𝐶, 𝑦𝐷𝑅))
2 ovmpod.2 . 2 ((𝜑 ∧ (𝑥 = 𝐴𝑦 = 𝐵)) → 𝑅 = 𝑆)
3 eqidd 2799 . 2 ((𝜑𝑥 = 𝐴) → 𝐷 = 𝐷)
4 ovmpod.3 . 2 (𝜑𝐴𝐶)
5 ovmpod.4 . 2 (𝜑𝐵𝐷)
6 ovmpod.5 . 2 (𝜑𝑆𝑋)
71, 2, 3, 4, 5, 6ovmpodx 7291 1 (𝜑 → (𝐴𝐹𝐵) = 𝑆)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  (class class class)co 7145   ∈ cmpo 7147 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5171  ax-nul 5178  ax-pr 5299 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-v 3444  df-sbc 3723  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4805  df-br 5035  df-opab 5097  df-id 5429  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-iota 6291  df-fun 6334  df-fv 6340  df-ov 7148  df-oprab 7149  df-mpo 7150 This theorem is referenced by:  ovmpoga  7294  fvmpopr2d  7301  el2mpocsbcl  7776  fsplitfpar  7810  suppval  7828  sprmpod  7891  mpocurryd  7936  erov  8395  cnfcomlem  9164  swrdval  14016  pfxval  14046  splval  14124  0csh0  14166  relexp0g  14393  relexpsucnnr  14396  relexp1g  14397  ramval  16354  prdsval  16740  prdsplusgval  16758  prdsmulrval  16760  prdsdsval  16763  prdsvscaval  16764  imasval  16796  imasdsval  16800  qusval  16827  homfval  16974  comffval  16981  comfval  16982  oppccofval  16998  ismon  17015  sectfval  17033  invfval  17041  cofuval  17164  cofu2nd  17167  resfval  17174  isnat  17229  fucval  17240  fucco  17244  setchom  17352  setcco  17355  catchom  17371  catcco  17373  estrchom  17389  estrcco  17392  funcestrcsetclem5  17406  funcsetcestrclem5  17421  xpcval  17439  xpcid  17451  1stf2  17455  2ndf2  17458  prfval  17461  prf2fval  17463  evlfval  17479  evlf2  17480  evlf2val  17481  evlf1  17482  curfval  17485  uncfval  17496  diagval  17502  hof2fval  17517  hof2val  17518  yonedalem4a  17537  gsumvalx  17898  mgm2nsgrplem2  18096  mgm2nsgrplem3  18097  sgrp2nmndlem2  18101  sgrp2nmndlem3  18102  pwmndgplus  18112  symgov  18525  pj1fval  18833  isrim0  19492  rmodislmodlem  19715  rmodislmod  19716  frlmphl  20492  uvcfval  20495  psrval  20623  selvffval  20825  mamufval  21033  mamuval  21034  mamufv  21035  matinvgcell  21081  mpomatmul  21092  mat1ov  21094  dmatval  21138  dmatmulcl  21146  scmatval  21150  scmatscmiddistr  21154  scmatscm  21159  mvmulfval  21188  mvmulval  21189  1mavmul  21194  maducoeval  21285  symgmatr01  21300  gsummatr01lem3  21303  gsummatr01lem4  21304  gsummatr01  21305  cpmat  21355  mat2pmatfval  21369  mat2pmatvalel  21371  mat2pmatmul  21377  cpm2mfval  21395  cpm2mvalel  21397  m2cpminvid  21399  m2cpminvid2  21401  decpmatval0  21410  decpmate  21412  decpmataa0  21414  decpmatmul  21418  pmatcollpw1  21422  monmatcollpw  21425  pmatcollpwlem  21426  pmatcollpw  21427  pmatcollpwscmatlem2  21436  pm2mpval  21441  pm2mpf1  21445  mptcoe1matfsupp  21448  mp2pm2mplem3  21454  mp2pm2mplem4  21455  chmatval  21475  chpmatfval  21476  chp0mat  21492  cnfval  21879  cnpfval  21880  fmval  22589  fmf  22591  fcfval  22679  tsmsval2  22776  blvalps  23033  blval  23034  ishtpy  23618  isphtpy  23627  rrxnm  24036  rrxmval  24050  rrxdsfival  24058  ehl2eudisval  24068  limcfval  24516  q1pval  24798  r1pval  24801  ismidb  26616  ttgitvval  26720  ebtwntg  26820  ecgrtg  26821  ewlksfval  27435  wwlksnon  27681  wspthsnon  27682  iswwlksnon  27683  iswspthsnon  27686  numclwlk1lem2  28199  ofoprabco  30471  mntoval  30734  mgcoval  30738  idlsrgmulrval  31123  fedgmul  31181  smatfval  31214  lmatfval  31233  mdetpmtr1  31242  ofcfval  31533  sitmfval  31784  sseqval  31822  sseqf  31826  sseqp1  31829  cndprobval  31867  orvcval  31891  reprval  32057  lpadval  32123  satf  32779  satefv  32840  mclsval  32989  fwddifnval  33884  bj-imdirvallem  34746  finxpreclem1  34957  finxpreclem3  34961  ismtyval  35389  rrnmval  35417  rfovd  40873  fsovd  40880  fsovrfovd  40881  mnringmulrvald  41106  bccval  41213  fmuldfeqlem1  42392  rrndistlt  43100  hoidmvval  43384  hspval  43416  hoiqssbllem2  43430  smflimlem3  43574  copissgrp  44596  copisnmnd  44597  intopval  44630  rnghmval  44683  isrngisom  44688  rhmval  44711  cznrng  44747  rnghmsscmap2  44765  rnghmsscmap  44766  rngchomALTV  44777  rngccoALTV  44780  funcrngcsetc  44790  funcrngcsetcALT  44791  rhmsscmap2  44811  rhmsscmap  44812  funcringcsetc  44827  funcringcsetcALTV2lem5  44832  ringchomALTV  44840  ringccoALTV  44843  funcringcsetclem5ALTV  44855  srhmsubclem3  44867  srhmsubc  44868  fldhmsubc  44876  srhmsubcALTVlem2  44885  srhmsubcALTV  44886  fldhmsubcALTV  44894  lmod1lem1  45062  lmod1lem2  45063  lmod1lem3  45064  lmod1lem4  45065  lmod1lem5  45066  fdivval  45119  digval  45178  itcoval1  45243  itcoval2  45244  itcoval3  45245  itcovalsucov  45248  ackvalsuc1mpt  45258  rrx2plordisom  45303  sphere  45327
 Copyright terms: Public domain W3C validator