Theorem ovmpod 7602

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2108  (class class class)co 7448   ∈ cmpo 7450

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-iota 6525  df-fun 6575  df-fv 6581  df-ov 7451  df-oprab 7452  df-mpo 7453

This theorem is referenced by:  ovmpoga  7604  fvmpopr2d  7612  elovmpod  7694  el2mpocsbcl  8126  fsplitfpar  8159  suppval  8203  sprmpod  8265  mpocurryd  8310  erov  8872  cnfcomlem  9768  swrdval  14691  pfxval  14721  splval  14799  0csh0  14841  relexp0g  15071  relexpsucnnr  15074  relexp1g  15075  ramval  17055  prdsval  17515  prdsplusgval  17533  prdsmulrval  17535  prdsdsval  17538  prdsvscaval  17539  imasval  17571  imasdsval  17575  qusval  17602  homfval  17750  comffval  17757  comfval  17758  oppccofval  17775  ismon  17794  sectfval  17812  invfval  17820  cofuval  17946  cofu2nd  17949  resfval  17956  isnat  18015  fucval  18027  fucco  18032  setchom  18147  setcco  18150  catchom  18170  catcco  18172  estrchom  18195  estrcco  18198  funcestrcsetclem5  18213  funcsetcestrclem5  18228  xpcval  18246  xpcid  18258  1stf2  18262  2ndf2  18265  prfval  18268  prf2fval  18270  evlfval  18287  evlf2  18288  evlf2val  18289  evlf1  18290  curfval  18293  uncfval  18304  diagval  18310  hof2fval  18325  hof2val  18326  yonedalem4a  18345  gsumvalx  18714  mgm2nsgrplem2  18954  mgm2nsgrplem3  18955  sgrp2nmndlem2  18959  sgrp2nmndlem3  18960  pwmndgplus  18970  symgov  19425  pj1fval  19736  rnghmval  20466  isrngim  20471  isrim0OLD  20507  isrim0  20509  rhmval  20526  rnghmsscmap2  20651  rnghmsscmap  20652  funcrngcsetc  20662  funcrngcsetcALT  20663  rhmsscmap2  20680  rhmsscmap  20681  funcringcsetc  20696  srhmsubclem3  20701  srhmsubc  20702  fldhmsubc  20808  rmodislmodlem  20949  rmodislmod  20950  rmodislmodOLD  20951  frlmphl  21824  uvcfval  21827  psrval  21958  selvffval  22160  psdffval  22184  mamufval  22417  mamuval  22418  mamufv  22419  matinvgcell  22462  mpomatmul  22473  mat1ov  22475  dmatval  22519  dmatmulcl  22527  scmatval  22531  scmatscmiddistr  22535  scmatscm  22540  mvmulfval  22569  mvmulval  22570  1mavmul  22575  maducoeval  22666  symgmatr01  22681  gsummatr01lem3  22684  gsummatr01lem4  22685  gsummatr01  22686  cpmat  22736  mat2pmatfval  22750  mat2pmatvalel  22752  mat2pmatmul  22758  cpm2mfval  22776  cpm2mvalel  22778  m2cpminvid  22780  m2cpminvid2  22782  decpmatval0  22791  decpmate  22793  decpmataa0  22795  decpmatmul  22799  pmatcollpw1  22803  monmatcollpw  22806  pmatcollpwlem  22807  pmatcollpw  22808  pmatcollpwscmatlem2  22817  pm2mpval  22822  pm2mpf1  22826  mptcoe1matfsupp  22829  mp2pm2mplem3  22835  mp2pm2mplem4  22836  chmatval  22856  chpmatfval  22857  chp0mat  22873  cnfval  23262  cnpfval  23263  fmval  23972  fmf  23974  fcfval  24062  tsmsval2  24159  blvalps  24416  blval  24417  ishtpy  25023  isphtpy  25032  rrxnm  25444  rrxmval  25458  rrxdsfival  25466  ehl2eudisval  25476  limcfval  25927  q1pval  26214  r1pval  26217  ismidb  28804  ttgitvval  28914  ebtwntg  29015  ecgrtg  29016  ewlksfval  29637  wwlksnon  29884  wspthsnon  29885  iswwlksnon  29886  iswspthsnon  29889  numclwlk1lem2  30402  ofoprabco  32682  of0r  32696  mntoval  32955  mgcoval  32959  rlocaddval  33240  rlocmulval  33241  idlsrgmulrval  33502  fedgmul  33644  smatfval  33741  lmatfval  33760  mdetpmtr1  33769  ofcfval  34062  sitmfval  34315  sseqval  34353  sseqf  34357  sseqp1  34360  cndprobval  34398  orvcval  34422  reprval  34587  lpadval  34653  satf  35321  satefv  35382  mclsval  35531  fwddifnval  36127  bj-imdirvallem  37146  finxpreclem1  37355  finxpreclem3  37359  ismtyval  37760  rrnmval  37788  isprimroot  42050  aks6d1c2p2  42076  aks6d1c2lem3  42083  aks6d1c2lem4  42084  aks6d1c6lem3  42129  ovmpogad  42230  tfsconcatun  43299  rfovd  43963  fsovd  43970  fsovrfovd  43971  mnringmulrvald  44196  bccval  44307  fmuldfeqlem1  45503  rrndistlt  46211  hoidmvval  46498  hspval  46530  hoiqssbllem2  46544  smflimlem3  46694  copissgrp  47891  copisnmnd  47892  intopval  47925  cznrng  47984  rngchomALTV  47991  rngccoALTV  47994  funcringcsetcALTV2lem5  48017  ringchomALTV  48025  ringccoALTV  48028  funcringcsetclem5ALTV  48040  srhmsubcALTVlem2  48047  srhmsubcALTV  48048  fldhmsubcALTV  48056  lmod1lem1  48216  lmod1lem2  48217  lmod1lem3  48218  lmod1lem4  48219  lmod1lem5  48220  fdivval  48273  digval  48332  itcoval1  48397  itcoval2  48398  itcoval3  48399  itcovalsucov  48402  ackvalsuc1mpt  48412  rrx2plordisom  48457  sphere  48481  functhinclem3  48710