Theorem ovmpod 7504

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 2732	. 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐷 = 𝐷)
4		ovmpod.3	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐶)
5		ovmpod.4	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐷)
6		ovmpod.5	. 2 ⊢ (𝜑 → 𝑆 ∈ 𝑋)
7	1, 2, 3, 4, 5, 6	ovmpodx 7503	1 ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111  (class class class)co 7352   ∈ cmpo 7354

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5236  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-iota 6443  df-fun 6489  df-fv 6495  df-ov 7355  df-oprab 7356  df-mpo 7357

This theorem is referenced by:  ovmpoga  7506  fvmpopr2d  7514  elovmpod  7596  el2mpocsbcl  8021  fsplitfpar  8054  suppval  8098  sprmpod  8160  mpocurryd  8205  erov  8744  cnfcomlem  9595  swrdval  14557  pfxval  14587  splval  14664  0csh0  14706  relexp0g  14935  relexpsucnnr  14938  relexp1g  14939  ramval  16926  prdsval  17365  prdsplusgval  17383  prdsmulrval  17385  prdsdsval  17388  prdsvscaval  17389  imasval  17421  imasdsval  17425  qusval  17452  homfval  17604  comffval  17611  comfval  17612  oppccofval  17628  ismon  17646  sectfval  17664  invfval  17672  cofuval  17795  cofu2nd  17798  resfval  17805  isnat  17863  fucval  17874  fucco  17878  setchom  17993  setcco  17996  catchom  18016  catcco  18018  estrchom  18039  estrcco  18042  funcestrcsetclem5  18056  funcsetcestrclem5  18071  xpcval  18089  xpcid  18101  1stf2  18105  2ndf2  18108  prfval  18111  prf2fval  18113  evlfval  18129  evlf2  18130  evlf2val  18131  evlf1  18132  curfval  18135  uncfval  18146  diagval  18152  hof2fval  18167  hof2val  18168  yonedalem4a  18187  gsumvalx  18590  mgm2nsgrplem2  18833  mgm2nsgrplem3  18834  sgrp2nmndlem2  18838  sgrp2nmndlem3  18839  pwmndgplus  18849  symgov  19302  pj1fval  19612  rnghmval  20364  isrngim  20369  isrim0  20406  rhmval  20421  rnghmsscmap2  20550  rnghmsscmap  20551  funcrngcsetc  20561  funcrngcsetcALT  20562  rhmsscmap2  20579  rhmsscmap  20580  funcringcsetc  20595  srhmsubclem3  20600  srhmsubc  20601  fldhmsubc  20706  rmodislmodlem  20868  rmodislmod  20869  frlmphl  21724  uvcfval  21727  psrval  21858  selvffval  22054  psdffval  22078  mamufval  22313  mamuval  22314  mamufv  22315  matinvgcell  22356  mpomatmul  22367  mat1ov  22369  dmatval  22413  dmatmulcl  22421  scmatval  22425  scmatscmiddistr  22429  scmatscm  22434  mvmulfval  22463  mvmulval  22464  1mavmul  22469  maducoeval  22560  symgmatr01  22575  gsummatr01lem3  22578  gsummatr01lem4  22579  gsummatr01  22580  cpmat  22630  mat2pmatfval  22644  mat2pmatvalel  22646  mat2pmatmul  22652  cpm2mfval  22670  cpm2mvalel  22672  m2cpminvid  22674  m2cpminvid2  22676  decpmatval0  22685  decpmate  22687  decpmataa0  22689  decpmatmul  22693  pmatcollpw1  22697  monmatcollpw  22700  pmatcollpwlem  22701  pmatcollpw  22702  pmatcollpwscmatlem2  22711  pm2mpval  22716  pm2mpf1  22720  mptcoe1matfsupp  22723  mp2pm2mplem3  22729  mp2pm2mplem4  22730  chmatval  22750  chpmatfval  22751  chp0mat  22767  cnfval  23154  cnpfval  23155  fmval  23864  fmf  23866  fcfval  23954  tsmsval2  24051  blvalps  24306  blval  24307  ishtpy  24904  isphtpy  24913  rrxnm  25324  rrxmval  25338  rrxdsfival  25346  ehl2eudisval  25356  limcfval  25806  q1pval  26093  r1pval  26096  ismidb  28762  ttgitvval  28866  ebtwntg  28967  ecgrtg  28968  ewlksfval  29587  wwlksnon  29836  wspthsnon  29837  iswwlksnon  29838  iswspthsnon  29841  numclwlk1lem2  30357  ofoprabco  32653  of0r  32667  mntoval  32970  mgcoval  32974  fxpval  33141  conjga  33146  cntrval2  33147  elrgspnlem2  33217  rlocaddval  33242  rlocmulval  33243  idlsrgmulrval  33481  mplvrpmfgalem  33581  mplvrpmga  33582  mplvrpmmhm  33583  mplvrpmrhm  33584  splyval  33589  issply  33591  esplyval  33592  fedgmul  33651  smatfval  33815  lmatfval  33834  mdetpmtr1  33843  ofcfval  34118  sitmfval  34370  sseqval  34408  sseqf  34412  sseqp1  34415  cndprobval  34453  orvcval  34478  reprval  34630  lpadval  34696  satf  35404  satefv  35465  mclsval  35614  fwddifnval  36214  bj-imdirvallem  37231  finxpreclem1  37440  finxpreclem3  37444  ismtyval  37846  rrnmval  37874  isprimroot  42192  aks6d1c2p2  42218  aks6d1c2lem3  42225  aks6d1c2lem4  42226  aks6d1c6lem3  42271  ovmpogad  42334  tfsconcatun  43435  rfovd  44099  fsovd  44106  fsovrfovd  44107  mnringmulrvald  44325  bccval  44436  fmuldfeqlem1  45687  rrndistlt  46393  hoidmvval  46680  hspval  46712  hoiqssbllem2  46726  smflimlem3  46876  copissgrp  48273  copisnmnd  48274  intopval  48307  cznrng  48366  rngchomALTV  48373  rngccoALTV  48376  funcringcsetcALTV2lem5  48399  ringchomALTV  48407  ringccoALTV  48410  funcringcsetclem5ALTV  48422  srhmsubcALTVlem2  48429  srhmsubcALTV  48430  fldhmsubcALTV  48438  lmod1lem1  48593  lmod1lem2  48594  lmod1lem3  48595  lmod1lem4  48596  lmod1lem5  48597  fdivval  48645  digval  48704  itcoval1  48769  itcoval2  48770  itcoval3  48771  itcovalsucov  48774  ackvalsuc1mpt  48784  rrx2plordisom  48829  sphere  48853  iinfssclem3  49162  swapfval  49368  swapf2vala  49376  fucofvalg  49424  fuco112x  49438  fuco21  49442  fuco22  49445  prcofvalg  49482  prcof2a  49495  prcof2  49496  opf2fval  49511  functhinclem3  49552  incat  49707  lanfval  49719  ranfval  49720  lanval  49725  ranval  49726