Theorem ovmpod 7541

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  (class class class)co 7387   ∈ cmpo 7389

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6464  df-fun 6513  df-fv 6519  df-ov 7390  df-oprab 7391  df-mpo 7392

This theorem is referenced by:  ovmpoga  7543  fvmpopr2d  7551  elovmpod  7633  el2mpocsbcl  8064  fsplitfpar  8097  suppval  8141  sprmpod  8203  mpocurryd  8248  erov  8787  cnfcomlem  9652  swrdval  14608  pfxval  14638  splval  14716  0csh0  14758  relexp0g  14988  relexpsucnnr  14991  relexp1g  14992  ramval  16979  prdsval  17418  prdsplusgval  17436  prdsmulrval  17438  prdsdsval  17441  prdsvscaval  17442  imasval  17474  imasdsval  17478  qusval  17505  homfval  17653  comffval  17660  comfval  17661  oppccofval  17677  ismon  17695  sectfval  17713  invfval  17721  cofuval  17844  cofu2nd  17847  resfval  17854  isnat  17912  fucval  17923  fucco  17927  setchom  18042  setcco  18045  catchom  18065  catcco  18067  estrchom  18088  estrcco  18091  funcestrcsetclem5  18105  funcsetcestrclem5  18120  xpcval  18138  xpcid  18150  1stf2  18154  2ndf2  18157  prfval  18160  prf2fval  18162  evlfval  18178  evlf2  18179  evlf2val  18180  evlf1  18181  curfval  18184  uncfval  18195  diagval  18201  hof2fval  18216  hof2val  18217  yonedalem4a  18236  gsumvalx  18603  mgm2nsgrplem2  18846  mgm2nsgrplem3  18847  sgrp2nmndlem2  18851  sgrp2nmndlem3  18852  pwmndgplus  18862  symgov  19314  pj1fval  19624  rnghmval  20349  isrngim  20354  isrim0OLD  20390  isrim0  20392  rhmval  20409  rnghmsscmap2  20538  rnghmsscmap  20539  funcrngcsetc  20549  funcrngcsetcALT  20550  rhmsscmap2  20567  rhmsscmap  20568  funcringcsetc  20583  srhmsubclem3  20588  srhmsubc  20589  fldhmsubc  20694  rmodislmodlem  20835  rmodislmod  20836  frlmphl  21690  uvcfval  21693  psrval  21824  selvffval  22020  psdffval  22044  mamufval  22279  mamuval  22280  mamufv  22281  matinvgcell  22322  mpomatmul  22333  mat1ov  22335  dmatval  22379  dmatmulcl  22387  scmatval  22391  scmatscmiddistr  22395  scmatscm  22400  mvmulfval  22429  mvmulval  22430  1mavmul  22435  maducoeval  22526  symgmatr01  22541  gsummatr01lem3  22544  gsummatr01lem4  22545  gsummatr01  22546  cpmat  22596  mat2pmatfval  22610  mat2pmatvalel  22612  mat2pmatmul  22618  cpm2mfval  22636  cpm2mvalel  22638  m2cpminvid  22640  m2cpminvid2  22642  decpmatval0  22651  decpmate  22653  decpmataa0  22655  decpmatmul  22659  pmatcollpw1  22663  monmatcollpw  22666  pmatcollpwlem  22667  pmatcollpw  22668  pmatcollpwscmatlem2  22677  pm2mpval  22682  pm2mpf1  22686  mptcoe1matfsupp  22689  mp2pm2mplem3  22695  mp2pm2mplem4  22696  chmatval  22716  chpmatfval  22717  chp0mat  22733  cnfval  23120  cnpfval  23121  fmval  23830  fmf  23832  fcfval  23920  tsmsval2  24017  blvalps  24273  blval  24274  ishtpy  24871  isphtpy  24880  rrxnm  25291  rrxmval  25305  rrxdsfival  25313  ehl2eudisval  25323  limcfval  25773  q1pval  26060  r1pval  26063  ismidb  28705  ttgitvval  28809  ebtwntg  28909  ecgrtg  28910  ewlksfval  29529  wwlksnon  29781  wspthsnon  29782  iswwlksnon  29783  iswspthsnon  29786  numclwlk1lem2  30299  ofoprabco  32588  of0r  32602  mntoval  32908  mgcoval  32912  fxpval  33122  conjga  33127  cntrval2  33128  elrgspnlem2  33194  rlocaddval  33219  rlocmulval  33220  idlsrgmulrval  33480  fedgmul  33627  smatfval  33785  lmatfval  33804  mdetpmtr1  33813  ofcfval  34088  sitmfval  34341  sseqval  34379  sseqf  34383  sseqp1  34386  cndprobval  34424  orvcval  34449  reprval  34601  lpadval  34667  satf  35340  satefv  35401  mclsval  35550  fwddifnval  36151  bj-imdirvallem  37168  finxpreclem1  37377  finxpreclem3  37381  ismtyval  37794  rrnmval  37822  isprimroot  42081  aks6d1c2p2  42107  aks6d1c2lem3  42114  aks6d1c2lem4  42115  aks6d1c6lem3  42160  ovmpogad  42223  tfsconcatun  43326  rfovd  43990  fsovd  43997  fsovrfovd  43998  mnringmulrvald  44216  bccval  44327  fmuldfeqlem1  45580  rrndistlt  46288  hoidmvval  46575  hspval  46607  hoiqssbllem2  46621  smflimlem3  46771  copissgrp  48156  copisnmnd  48157  intopval  48190  cznrng  48249  rngchomALTV  48256  rngccoALTV  48259  funcringcsetcALTV2lem5  48282  ringchomALTV  48290  ringccoALTV  48293  funcringcsetclem5ALTV  48305  srhmsubcALTVlem2  48312  srhmsubcALTV  48313  fldhmsubcALTV  48321  lmod1lem1  48476  lmod1lem2  48477  lmod1lem3  48478  lmod1lem4  48479  lmod1lem5  48480  fdivval  48528  digval  48587  itcoval1  48652  itcoval2  48653  itcoval3  48654  itcovalsucov  48657  ackvalsuc1mpt  48667  rrx2plordisom  48712  sphere  48736  iinfssclem3  49045  swapfval  49251  swapf2vala  49259  fucofvalg  49307  fuco112x  49321  fuco21  49325  fuco22  49328  prcofvalg  49365  prcof2a  49378  prcof2  49379  opf2fval  49394  functhinclem3  49435  incat  49590  lanfval  49602  ranfval  49603  lanval  49608  ranval  49609