Theorem ovmpod 7559

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

Step	Hyp	Ref	Expression
1		ovmpod.1	. 2 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐶, 𝑦 ∈ 𝐷 ↦ 𝑅))
2		ovmpod.2	. 2 ⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → 𝑅 = 𝑆)
3		eqidd 2736	. 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐷 = 𝐷)
4		ovmpod.3	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐶)
5		ovmpod.4	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐷)
6		ovmpod.5	. 2 ⊢ (𝜑 → 𝑆 ∈ 𝑋)
7	1, 2, 3, 4, 5, 6	ovmpodx 7558	1 ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  (class class class)co 7405   ∈ cmpo 7407

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-iota 6484  df-fun 6533  df-fv 6539  df-ov 7408  df-oprab 7409  df-mpo 7410

This theorem is referenced by:  ovmpoga  7561  fvmpopr2d  7569  elovmpod  7651  el2mpocsbcl  8084  fsplitfpar  8117  suppval  8161  sprmpod  8223  mpocurryd  8268  erov  8828  cnfcomlem  9713  swrdval  14661  pfxval  14691  splval  14769  0csh0  14811  relexp0g  15041  relexpsucnnr  15044  relexp1g  15045  ramval  17028  prdsval  17469  prdsplusgval  17487  prdsmulrval  17489  prdsdsval  17492  prdsvscaval  17493  imasval  17525  imasdsval  17529  qusval  17556  homfval  17704  comffval  17711  comfval  17712  oppccofval  17728  ismon  17746  sectfval  17764  invfval  17772  cofuval  17895  cofu2nd  17898  resfval  17905  isnat  17963  fucval  17974  fucco  17978  setchom  18093  setcco  18096  catchom  18116  catcco  18118  estrchom  18139  estrcco  18142  funcestrcsetclem5  18156  funcsetcestrclem5  18171  xpcval  18189  xpcid  18201  1stf2  18205  2ndf2  18208  prfval  18211  prf2fval  18213  evlfval  18229  evlf2  18230  evlf2val  18231  evlf1  18232  curfval  18235  uncfval  18246  diagval  18252  hof2fval  18267  hof2val  18268  yonedalem4a  18287  gsumvalx  18654  mgm2nsgrplem2  18897  mgm2nsgrplem3  18898  sgrp2nmndlem2  18902  sgrp2nmndlem3  18903  pwmndgplus  18913  symgov  19365  pj1fval  19675  rnghmval  20400  isrngim  20405  isrim0OLD  20441  isrim0  20443  rhmval  20460  rnghmsscmap2  20589  rnghmsscmap  20590  funcrngcsetc  20600  funcrngcsetcALT  20601  rhmsscmap2  20618  rhmsscmap  20619  funcringcsetc  20634  srhmsubclem3  20639  srhmsubc  20640  fldhmsubc  20745  rmodislmodlem  20886  rmodislmod  20887  frlmphl  21741  uvcfval  21744  psrval  21875  selvffval  22071  psdffval  22095  mamufval  22330  mamuval  22331  mamufv  22332  matinvgcell  22373  mpomatmul  22384  mat1ov  22386  dmatval  22430  dmatmulcl  22438  scmatval  22442  scmatscmiddistr  22446  scmatscm  22451  mvmulfval  22480  mvmulval  22481  1mavmul  22486  maducoeval  22577  symgmatr01  22592  gsummatr01lem3  22595  gsummatr01lem4  22596  gsummatr01  22597  cpmat  22647  mat2pmatfval  22661  mat2pmatvalel  22663  mat2pmatmul  22669  cpm2mfval  22687  cpm2mvalel  22689  m2cpminvid  22691  m2cpminvid2  22693  decpmatval0  22702  decpmate  22704  decpmataa0  22706  decpmatmul  22710  pmatcollpw1  22714  monmatcollpw  22717  pmatcollpwlem  22718  pmatcollpw  22719  pmatcollpwscmatlem2  22728  pm2mpval  22733  pm2mpf1  22737  mptcoe1matfsupp  22740  mp2pm2mplem3  22746  mp2pm2mplem4  22747  chmatval  22767  chpmatfval  22768  chp0mat  22784  cnfval  23171  cnpfval  23172  fmval  23881  fmf  23883  fcfval  23971  tsmsval2  24068  blvalps  24324  blval  24325  ishtpy  24922  isphtpy  24931  rrxnm  25343  rrxmval  25357  rrxdsfival  25365  ehl2eudisval  25375  limcfval  25825  q1pval  26112  r1pval  26115  ismidb  28757  ttgitvval  28861  ebtwntg  28961  ecgrtg  28962  ewlksfval  29581  wwlksnon  29833  wspthsnon  29834  iswwlksnon  29835  iswspthsnon  29838  numclwlk1lem2  30351  ofoprabco  32642  of0r  32656  mntoval  32962  mgcoval  32966  elrgspnlem2  33238  rlocaddval  33263  rlocmulval  33264  idlsrgmulrval  33524  fedgmul  33671  smatfval  33826  lmatfval  33845  mdetpmtr1  33854  ofcfval  34129  sitmfval  34382  sseqval  34420  sseqf  34424  sseqp1  34427  cndprobval  34465  orvcval  34490  reprval  34642  lpadval  34708  satf  35375  satefv  35436  mclsval  35585  fwddifnval  36181  bj-imdirvallem  37198  finxpreclem1  37407  finxpreclem3  37411  ismtyval  37824  rrnmval  37852  isprimroot  42106  aks6d1c2p2  42132  aks6d1c2lem3  42139  aks6d1c2lem4  42140  aks6d1c6lem3  42185  ovmpogad  42286  tfsconcatun  43361  rfovd  44025  fsovd  44032  fsovrfovd  44033  mnringmulrvald  44251  bccval  44362  fmuldfeqlem1  45611  rrndistlt  46319  hoidmvval  46606  hspval  46638  hoiqssbllem2  46652  smflimlem3  46802  copissgrp  48143  copisnmnd  48144  intopval  48177  cznrng  48236  rngchomALTV  48243  rngccoALTV  48246  funcringcsetcALTV2lem5  48269  ringchomALTV  48277  ringccoALTV  48280  funcringcsetclem5ALTV  48292  srhmsubcALTVlem2  48299  srhmsubcALTV  48300  fldhmsubcALTV  48308  lmod1lem1  48463  lmod1lem2  48464  lmod1lem3  48465  lmod1lem4  48466  lmod1lem5  48467  fdivval  48519  digval  48578  itcoval1  48643  itcoval2  48644  itcoval3  48645  itcovalsucov  48648  ackvalsuc1mpt  48658  rrx2plordisom  48703  sphere  48727  iinfssclem3  49023  swapfval  49179  swapf2vala  49187  fucofvalg  49229  fuco112x  49243  fuco21  49247  fuco22  49250  prcofvalg  49287  prcof2a  49299  prcof2  49300  functhinclem3  49332  incat  49478  lanfval  49490  ranfval  49491  lanval  49494  ranval  49495