Theorem ovmpod 7361

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543   ∈ wcel 2110  (class class class)co 7213   ∈ cmpo 7215

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-sbc 3695  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-opab 5116  df-id 5455  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-iota 6338  df-fun 6382  df-fv 6388  df-ov 7216  df-oprab 7217  df-mpo 7218

This theorem is referenced by:  ovmpoga  7363  fvmpopr2d  7370  el2mpocsbcl  7853  fsplitfpar  7887  suppval  7905  sprmpod  7966  mpocurryd  8011  erov  8496  cnfcomlem  9314  swrdval  14208  pfxval  14238  splval  14316  0csh0  14358  relexp0g  14585  relexpsucnnr  14588  relexp1g  14589  ramval  16561  prdsval  16960  prdsplusgval  16978  prdsmulrval  16980  prdsdsval  16983  prdsvscaval  16984  imasval  17016  imasdsval  17020  qusval  17047  homfval  17195  comffval  17202  comfval  17203  oppccofval  17220  ismon  17238  sectfval  17256  invfval  17264  cofuval  17388  cofu2nd  17391  resfval  17398  isnat  17454  fucval  17466  fucco  17471  setchom  17586  setcco  17589  catchom  17609  catcco  17611  estrchom  17634  estrcco  17637  funcestrcsetclem5  17651  funcsetcestrclem5  17666  xpcval  17684  xpcid  17696  1stf2  17700  2ndf2  17703  prfval  17706  prf2fval  17708  evlfval  17725  evlf2  17726  evlf2val  17727  evlf1  17728  curfval  17731  uncfval  17742  diagval  17748  hof2fval  17763  hof2val  17764  yonedalem4a  17783  gsumvalx  18148  mgm2nsgrplem2  18346  mgm2nsgrplem3  18347  sgrp2nmndlem2  18351  sgrp2nmndlem3  18352  pwmndgplus  18362  symgov  18776  pj1fval  19084  isrim0  19743  rmodislmodlem  19966  rmodislmod  19967  frlmphl  20743  uvcfval  20746  psrval  20874  selvffval  21076  mamufval  21284  mamuval  21285  mamufv  21286  matinvgcell  21332  mpomatmul  21343  mat1ov  21345  dmatval  21389  dmatmulcl  21397  scmatval  21401  scmatscmiddistr  21405  scmatscm  21410  mvmulfval  21439  mvmulval  21440  1mavmul  21445  maducoeval  21536  symgmatr01  21551  gsummatr01lem3  21554  gsummatr01lem4  21555  gsummatr01  21556  cpmat  21606  mat2pmatfval  21620  mat2pmatvalel  21622  mat2pmatmul  21628  cpm2mfval  21646  cpm2mvalel  21648  m2cpminvid  21650  m2cpminvid2  21652  decpmatval0  21661  decpmate  21663  decpmataa0  21665  decpmatmul  21669  pmatcollpw1  21673  monmatcollpw  21676  pmatcollpwlem  21677  pmatcollpw  21678  pmatcollpwscmatlem2  21687  pm2mpval  21692  pm2mpf1  21696  mptcoe1matfsupp  21699  mp2pm2mplem3  21705  mp2pm2mplem4  21706  chmatval  21726  chpmatfval  21727  chp0mat  21743  cnfval  22130  cnpfval  22131  fmval  22840  fmf  22842  fcfval  22930  tsmsval2  23027  blvalps  23283  blval  23284  ishtpy  23869  isphtpy  23878  rrxnm  24288  rrxmval  24302  rrxdsfival  24310  ehl2eudisval  24320  limcfval  24769  q1pval  25051  r1pval  25054  ismidb  26869  ttgitvval  26973  ebtwntg  27073  ecgrtg  27074  ewlksfval  27689  wwlksnon  27935  wspthsnon  27936  iswwlksnon  27937  iswspthsnon  27940  numclwlk1lem2  28453  ofoprabco  30721  mntoval  30979  mgcoval  30983  idlsrgmulrval  31368  fedgmul  31426  smatfval  31459  lmatfval  31478  mdetpmtr1  31487  ofcfval  31778  sitmfval  32029  sseqval  32067  sseqf  32071  sseqp1  32074  cndprobval  32112  orvcval  32136  reprval  32302  lpadval  32368  satf  33028  satefv  33089  mclsval  33238  fwddifnval  34202  bj-imdirvallem  35086  finxpreclem1  35297  finxpreclem3  35301  ismtyval  35695  rrnmval  35723  rfovd  41286  fsovd  41293  fsovrfovd  41294  mnringmulrvald  41518  bccval  41629  fmuldfeqlem1  42798  rrndistlt  43506  hoidmvval  43790  hspval  43822  hoiqssbllem2  43836  smflimlem3  43980  copissgrp  45035  copisnmnd  45036  intopval  45069  rnghmval  45122  isrngisom  45127  rhmval  45150  cznrng  45186  rnghmsscmap2  45204  rnghmsscmap  45205  rngchomALTV  45216  rngccoALTV  45219  funcrngcsetc  45229  funcrngcsetcALT  45230  rhmsscmap2  45250  rhmsscmap  45251  funcringcsetc  45266  funcringcsetcALTV2lem5  45271  ringchomALTV  45279  ringccoALTV  45282  funcringcsetclem5ALTV  45294  srhmsubclem3  45306  srhmsubc  45307  fldhmsubc  45315  srhmsubcALTVlem2  45324  srhmsubcALTV  45325  fldhmsubcALTV  45333  lmod1lem1  45501  lmod1lem2  45502  lmod1lem3  45503  lmod1lem4  45504  lmod1lem5  45505  fdivval  45558  digval  45617  itcoval1  45682  itcoval2  45683  itcoval3  45684  itcovalsucov  45687  ackvalsuc1mpt  45697  rrx2plordisom  45742  sphere  45766  functhinclem3  45997