Theorem ovmpod 7512

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 7511	1 ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  (class class class)co 7360   ∈ cmpo 7362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  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 7363  df-oprab 7364  df-mpo 7365

This theorem is referenced by:  ovmpoga  7514  fvmpopr2d  7522  elovmpod  7604  el2mpocsbcl  8028  fsplitfpar  8061  suppval  8105  sprmpod  8167  mpocurryd  8212  erov  8754  cnfcomlem  9611  swrdval  14597  pfxval  14627  splval  14704  0csh0  14746  relexp0g  14975  relexpsucnnr  14978  relexp1g  14979  ramval  16970  prdsval  17409  prdsplusgval  17427  prdsmulrval  17429  prdsdsval  17432  prdsvscaval  17433  imasval  17466  imasdsval  17470  qusval  17497  homfval  17649  comffval  17656  comfval  17657  oppccofval  17673  ismon  17691  sectfval  17709  invfval  17717  cofuval  17840  cofu2nd  17843  resfval  17850  isnat  17908  fucval  17919  fucco  17923  setchom  18038  setcco  18041  catchom  18061  catcco  18063  estrchom  18084  estrcco  18087  funcestrcsetclem5  18101  funcsetcestrclem5  18116  xpcval  18134  xpcid  18146  1stf2  18150  2ndf2  18153  prfval  18156  prf2fval  18158  evlfval  18174  evlf2  18175  evlf2val  18176  evlf1  18177  curfval  18180  uncfval  18191  diagval  18197  hof2fval  18212  hof2val  18213  yonedalem4a  18232  gsumvalx  18635  mgm2nsgrplem2  18881  mgm2nsgrplem3  18882  sgrp2nmndlem2  18886  sgrp2nmndlem3  18887  pwmndgplus  18897  symgov  19350  pj1fval  19660  rnghmval  20411  isrngim  20416  isrim0  20453  rhmval  20468  rnghmsscmap2  20597  rnghmsscmap  20598  funcrngcsetc  20608  funcrngcsetcALT  20609  rhmsscmap2  20626  rhmsscmap  20627  funcringcsetc  20642  srhmsubclem3  20647  srhmsubc  20648  fldhmsubc  20753  rmodislmodlem  20915  rmodislmod  20916  frlmphl  21771  uvcfval  21774  psrval  21905  selvffval  22109  psdffval  22133  mamufval  22367  mamuval  22368  mamufv  22369  matinvgcell  22410  mpomatmul  22421  mat1ov  22423  dmatval  22467  dmatmulcl  22475  scmatval  22479  scmatscmiddistr  22483  scmatscm  22488  mvmulfval  22517  mvmulval  22518  1mavmul  22523  maducoeval  22614  symgmatr01  22629  gsummatr01lem3  22632  gsummatr01lem4  22633  gsummatr01  22634  cpmat  22684  mat2pmatfval  22698  mat2pmatvalel  22700  mat2pmatmul  22706  cpm2mfval  22724  cpm2mvalel  22726  m2cpminvid  22728  m2cpminvid2  22730  decpmatval0  22739  decpmate  22741  decpmataa0  22743  decpmatmul  22747  pmatcollpw1  22751  monmatcollpw  22754  pmatcollpwlem  22755  pmatcollpw  22756  pmatcollpwscmatlem2  22765  pm2mpval  22770  pm2mpf1  22774  mptcoe1matfsupp  22777  mp2pm2mplem3  22783  mp2pm2mplem4  22784  chmatval  22804  chpmatfval  22805  chp0mat  22821  cnfval  23208  cnpfval  23209  fmval  23918  fmf  23920  fcfval  24008  tsmsval2  24105  blvalps  24360  blval  24361  ishtpy  24949  isphtpy  24958  rrxnm  25368  rrxmval  25382  rrxdsfival  25390  ehl2eudisval  25400  limcfval  25849  q1pval  26130  r1pval  26133  ismidb  28860  ttgitvval  28964  ebtwntg  29065  ecgrtg  29066  ewlksfval  29685  wwlksnon  29934  wspthsnon  29935  iswwlksnon  29936  iswspthsnon  29939  numclwlk1lem2  30455  ofoprabco  32752  of0r  32767  mntoval  33057  mgcoval  33061  fxpval  33241  conjga  33246  cntrval2  33247  elrgspnlem2  33319  rlocaddval  33344  rlocmulval  33345  idlsrgmulrval  33584  extvval  33690  mplvrpmfgalem  33703  mplvrpmga  33704  mplvrpmmhm  33705  mplvrpmrhm  33706  splyval  33718  issply  33720  esplyval  33721  fedgmul  33791  smatfval  33955  lmatfval  33974  mdetpmtr1  33983  ofcfval  34258  sitmfval  34510  sseqval  34548  sseqf  34552  sseqp1  34555  cndprobval  34593  orvcval  34618  reprval  34770  lpadval  34836  satf  35551  satefv  35612  mclsval  35761  fwddifnval  36361  bj-imdirvallem  37510  finxpreclem1  37719  finxpreclem3  37723  ismtyval  38135  rrnmval  38163  isprimroot  42546  aks6d1c2p2  42572  aks6d1c2lem3  42579  aks6d1c2lem4  42580  aks6d1c6lem3  42625  ovmpogad  42690  tfsconcatun  43783  rfovd  44446  fsovd  44453  fsovrfovd  44454  mnringmulrvald  44672  bccval  44783  fmuldfeqlem1  46030  rrndistlt  46736  hoidmvval  47023  hspval  47055  hoiqssbllem2  47069  smflimlem3  47219  copissgrp  48656  copisnmnd  48657  intopval  48690  cznrng  48749  rngchomALTV  48756  rngccoALTV  48759  funcringcsetcALTV2lem5  48782  ringchomALTV  48790  ringccoALTV  48793  funcringcsetclem5ALTV  48805  srhmsubcALTVlem2  48812  srhmsubcALTV  48813  fldhmsubcALTV  48821  lmod1lem1  48975  lmod1lem2  48976  lmod1lem3  48977  lmod1lem4  48978  lmod1lem5  48979  fdivval  49027  digval  49086  itcoval1  49151  itcoval2  49152  itcoval3  49153  itcovalsucov  49156  ackvalsuc1mpt  49166  rrx2plordisom  49211  sphere  49235  iinfssclem3  49543  swapfval  49749  swapf2vala  49757  fucofvalg  49805  fuco112x  49819  fuco21  49823  fuco22  49826  prcofvalg  49863  prcof2a  49876  prcof2  49877  opf2fval  49892  functhinclem3  49933  incat  50088  lanfval  50100  ranfval  50101  lanval  50106  ranval  50107