Theorem ovmpod 7544

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

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

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-iota 6467  df-fun 6516  df-fv 6522  df-ov 7393  df-oprab 7394  df-mpo 7395

This theorem is referenced by:  ovmpoga  7546  fvmpopr2d  7554  elovmpod  7636  el2mpocsbcl  8067  fsplitfpar  8100  suppval  8144  sprmpod  8206  mpocurryd  8251  erov  8790  cnfcomlem  9659  swrdval  14615  pfxval  14645  splval  14723  0csh0  14765  relexp0g  14995  relexpsucnnr  14998  relexp1g  14999  ramval  16986  prdsval  17425  prdsplusgval  17443  prdsmulrval  17445  prdsdsval  17448  prdsvscaval  17449  imasval  17481  imasdsval  17485  qusval  17512  homfval  17660  comffval  17667  comfval  17668  oppccofval  17684  ismon  17702  sectfval  17720  invfval  17728  cofuval  17851  cofu2nd  17854  resfval  17861  isnat  17919  fucval  17930  fucco  17934  setchom  18049  setcco  18052  catchom  18072  catcco  18074  estrchom  18095  estrcco  18098  funcestrcsetclem5  18112  funcsetcestrclem5  18127  xpcval  18145  xpcid  18157  1stf2  18161  2ndf2  18164  prfval  18167  prf2fval  18169  evlfval  18185  evlf2  18186  evlf2val  18187  evlf1  18188  curfval  18191  uncfval  18202  diagval  18208  hof2fval  18223  hof2val  18224  yonedalem4a  18243  gsumvalx  18610  mgm2nsgrplem2  18853  mgm2nsgrplem3  18854  sgrp2nmndlem2  18858  sgrp2nmndlem3  18859  pwmndgplus  18869  symgov  19321  pj1fval  19631  rnghmval  20356  isrngim  20361  isrim0OLD  20397  isrim0  20399  rhmval  20416  rnghmsscmap2  20545  rnghmsscmap  20546  funcrngcsetc  20556  funcrngcsetcALT  20557  rhmsscmap2  20574  rhmsscmap  20575  funcringcsetc  20590  srhmsubclem3  20595  srhmsubc  20596  fldhmsubc  20701  rmodislmodlem  20842  rmodislmod  20843  frlmphl  21697  uvcfval  21700  psrval  21831  selvffval  22027  psdffval  22051  mamufval  22286  mamuval  22287  mamufv  22288  matinvgcell  22329  mpomatmul  22340  mat1ov  22342  dmatval  22386  dmatmulcl  22394  scmatval  22398  scmatscmiddistr  22402  scmatscm  22407  mvmulfval  22436  mvmulval  22437  1mavmul  22442  maducoeval  22533  symgmatr01  22548  gsummatr01lem3  22551  gsummatr01lem4  22552  gsummatr01  22553  cpmat  22603  mat2pmatfval  22617  mat2pmatvalel  22619  mat2pmatmul  22625  cpm2mfval  22643  cpm2mvalel  22645  m2cpminvid  22647  m2cpminvid2  22649  decpmatval0  22658  decpmate  22660  decpmataa0  22662  decpmatmul  22666  pmatcollpw1  22670  monmatcollpw  22673  pmatcollpwlem  22674  pmatcollpw  22675  pmatcollpwscmatlem2  22684  pm2mpval  22689  pm2mpf1  22693  mptcoe1matfsupp  22696  mp2pm2mplem3  22702  mp2pm2mplem4  22703  chmatval  22723  chpmatfval  22724  chp0mat  22740  cnfval  23127  cnpfval  23128  fmval  23837  fmf  23839  fcfval  23927  tsmsval2  24024  blvalps  24280  blval  24281  ishtpy  24878  isphtpy  24887  rrxnm  25298  rrxmval  25312  rrxdsfival  25320  ehl2eudisval  25330  limcfval  25780  q1pval  26067  r1pval  26070  ismidb  28712  ttgitvval  28816  ebtwntg  28916  ecgrtg  28917  ewlksfval  29536  wwlksnon  29788  wspthsnon  29789  iswwlksnon  29790  iswspthsnon  29793  numclwlk1lem2  30306  ofoprabco  32595  of0r  32609  mntoval  32915  mgcoval  32919  fxpval  33129  conjga  33134  cntrval2  33135  elrgspnlem2  33201  rlocaddval  33226  rlocmulval  33227  idlsrgmulrval  33487  fedgmul  33634  smatfval  33792  lmatfval  33811  mdetpmtr1  33820  ofcfval  34095  sitmfval  34348  sseqval  34386  sseqf  34390  sseqp1  34393  cndprobval  34431  orvcval  34456  reprval  34608  lpadval  34674  satf  35347  satefv  35408  mclsval  35557  fwddifnval  36158  bj-imdirvallem  37175  finxpreclem1  37384  finxpreclem3  37388  ismtyval  37801  rrnmval  37829  isprimroot  42088  aks6d1c2p2  42114  aks6d1c2lem3  42121  aks6d1c2lem4  42122  aks6d1c6lem3  42167  ovmpogad  42230  tfsconcatun  43333  rfovd  43997  fsovd  44004  fsovrfovd  44005  mnringmulrvald  44223  bccval  44334  fmuldfeqlem1  45587  rrndistlt  46295  hoidmvval  46582  hspval  46614  hoiqssbllem2  46628  smflimlem3  46778  copissgrp  48160  copisnmnd  48161  intopval  48194  cznrng  48253  rngchomALTV  48260  rngccoALTV  48263  funcringcsetcALTV2lem5  48286  ringchomALTV  48294  ringccoALTV  48297  funcringcsetclem5ALTV  48309  srhmsubcALTVlem2  48316  srhmsubcALTV  48317  fldhmsubcALTV  48325  lmod1lem1  48480  lmod1lem2  48481  lmod1lem3  48482  lmod1lem4  48483  lmod1lem5  48484  fdivval  48532  digval  48591  itcoval1  48656  itcoval2  48657  itcoval3  48658  itcovalsucov  48661  ackvalsuc1mpt  48671  rrx2plordisom  48716  sphere  48740  iinfssclem3  49049  swapfval  49255  swapf2vala  49263  fucofvalg  49311  fuco112x  49325  fuco21  49329  fuco22  49332  prcofvalg  49369  prcof2a  49382  prcof2  49383  opf2fval  49398  functhinclem3  49439  incat  49594  lanfval  49606  ranfval  49607  lanval  49612  ranval  49613