Theorem ovmpod 7510

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  (class class class)co 7358   ∈ cmpo 7360

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-iota 6448  df-fun 6494  df-fv 6500  df-ov 7361  df-oprab 7362  df-mpo 7363

This theorem is referenced by:  ovmpoga  7512  fvmpopr2d  7520  elovmpod  7602  el2mpocsbcl  8027  fsplitfpar  8060  suppval  8104  sprmpod  8166  mpocurryd  8211  erov  8751  cnfcomlem  9608  swrdval  14567  pfxval  14597  splval  14674  0csh0  14716  relexp0g  14945  relexpsucnnr  14948  relexp1g  14949  ramval  16936  prdsval  17375  prdsplusgval  17393  prdsmulrval  17395  prdsdsval  17398  prdsvscaval  17399  imasval  17432  imasdsval  17436  qusval  17463  homfval  17615  comffval  17622  comfval  17623  oppccofval  17639  ismon  17657  sectfval  17675  invfval  17683  cofuval  17806  cofu2nd  17809  resfval  17816  isnat  17874  fucval  17885  fucco  17889  setchom  18004  setcco  18007  catchom  18027  catcco  18029  estrchom  18050  estrcco  18053  funcestrcsetclem5  18067  funcsetcestrclem5  18082  xpcval  18100  xpcid  18112  1stf2  18116  2ndf2  18119  prfval  18122  prf2fval  18124  evlfval  18140  evlf2  18141  evlf2val  18142  evlf1  18143  curfval  18146  uncfval  18157  diagval  18163  hof2fval  18178  hof2val  18179  yonedalem4a  18198  gsumvalx  18601  mgm2nsgrplem2  18844  mgm2nsgrplem3  18845  sgrp2nmndlem2  18849  sgrp2nmndlem3  18850  pwmndgplus  18860  symgov  19313  pj1fval  19623  rnghmval  20376  isrngim  20381  isrim0  20418  rhmval  20433  rnghmsscmap2  20562  rnghmsscmap  20563  funcrngcsetc  20573  funcrngcsetcALT  20574  rhmsscmap2  20591  rhmsscmap  20592  funcringcsetc  20607  srhmsubclem3  20612  srhmsubc  20613  fldhmsubc  20718  rmodislmodlem  20880  rmodislmod  20881  frlmphl  21736  uvcfval  21739  psrval  21871  selvffval  22076  psdffval  22100  mamufval  22336  mamuval  22337  mamufv  22338  matinvgcell  22379  mpomatmul  22390  mat1ov  22392  dmatval  22436  dmatmulcl  22444  scmatval  22448  scmatscmiddistr  22452  scmatscm  22457  mvmulfval  22486  mvmulval  22487  1mavmul  22492  maducoeval  22583  symgmatr01  22598  gsummatr01lem3  22601  gsummatr01lem4  22602  gsummatr01  22603  cpmat  22653  mat2pmatfval  22667  mat2pmatvalel  22669  mat2pmatmul  22675  cpm2mfval  22693  cpm2mvalel  22695  m2cpminvid  22697  m2cpminvid2  22699  decpmatval0  22708  decpmate  22710  decpmataa0  22712  decpmatmul  22716  pmatcollpw1  22720  monmatcollpw  22723  pmatcollpwlem  22724  pmatcollpw  22725  pmatcollpwscmatlem2  22734  pm2mpval  22739  pm2mpf1  22743  mptcoe1matfsupp  22746  mp2pm2mplem3  22752  mp2pm2mplem4  22753  chmatval  22773  chpmatfval  22774  chp0mat  22790  cnfval  23177  cnpfval  23178  fmval  23887  fmf  23889  fcfval  23977  tsmsval2  24074  blvalps  24329  blval  24330  ishtpy  24927  isphtpy  24936  rrxnm  25347  rrxmval  25361  rrxdsfival  25369  ehl2eudisval  25379  limcfval  25829  q1pval  26116  r1pval  26119  ismidb  28850  ttgitvval  28954  ebtwntg  29055  ecgrtg  29056  ewlksfval  29675  wwlksnon  29924  wspthsnon  29925  iswwlksnon  29926  iswspthsnon  29929  numclwlk1lem2  30445  ofoprabco  32742  of0r  32758  mntoval  33064  mgcoval  33068  fxpval  33247  conjga  33252  cntrval2  33253  elrgspnlem2  33325  rlocaddval  33350  rlocmulval  33351  idlsrgmulrval  33590  extvval  33696  mplvrpmfgalem  33709  mplvrpmga  33710  mplvrpmmhm  33711  mplvrpmrhm  33712  splyval  33717  issply  33719  esplyval  33720  fedgmul  33788  smatfval  33952  lmatfval  33971  mdetpmtr1  33980  ofcfval  34255  sitmfval  34507  sseqval  34545  sseqf  34549  sseqp1  34552  cndprobval  34590  orvcval  34615  reprval  34767  lpadval  34833  satf  35547  satefv  35608  mclsval  35757  fwddifnval  36357  bj-imdirvallem  37381  finxpreclem1  37590  finxpreclem3  37594  ismtyval  37997  rrnmval  38025  isprimroot  42343  aks6d1c2p2  42369  aks6d1c2lem3  42376  aks6d1c2lem4  42377  aks6d1c6lem3  42422  ovmpogad  42487  tfsconcatun  43575  rfovd  44238  fsovd  44245  fsovrfovd  44246  mnringmulrvald  44464  bccval  44575  fmuldfeqlem1  45824  rrndistlt  46530  hoidmvval  46817  hspval  46849  hoiqssbllem2  46863  smflimlem3  47013  copissgrp  48410  copisnmnd  48411  intopval  48444  cznrng  48503  rngchomALTV  48510  rngccoALTV  48513  funcringcsetcALTV2lem5  48536  ringchomALTV  48544  ringccoALTV  48547  funcringcsetclem5ALTV  48559  srhmsubcALTVlem2  48566  srhmsubcALTV  48567  fldhmsubcALTV  48575  lmod1lem1  48729  lmod1lem2  48730  lmod1lem3  48731  lmod1lem4  48732  lmod1lem5  48733  fdivval  48781  digval  48840  itcoval1  48905  itcoval2  48906  itcoval3  48907  itcovalsucov  48910  ackvalsuc1mpt  48920  rrx2plordisom  48965  sphere  48989  iinfssclem3  49297  swapfval  49503  swapf2vala  49511  fucofvalg  49559  fuco112x  49573  fuco21  49577  fuco22  49580  prcofvalg  49617  prcof2a  49630  prcof2  49631  opf2fval  49646  functhinclem3  49687  incat  49842  lanfval  49854  ranfval  49855  lanval  49860  ranval  49861