Theorem ovmpod 7584

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536   ∈ wcel 2105  (class class class)co 7430   ∈ cmpo 7432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-iota 6515  df-fun 6564  df-fv 6570  df-ov 7433  df-oprab 7434  df-mpo 7435

This theorem is referenced by:  ovmpoga  7586  fvmpopr2d  7594  elovmpod  7676  el2mpocsbcl  8108  fsplitfpar  8141  suppval  8185  sprmpod  8247  mpocurryd  8292  erov  8852  cnfcomlem  9736  swrdval  14677  pfxval  14707  splval  14785  0csh0  14827  relexp0g  15057  relexpsucnnr  15060  relexp1g  15061  ramval  17041  prdsval  17501  prdsplusgval  17519  prdsmulrval  17521  prdsdsval  17524  prdsvscaval  17525  imasval  17557  imasdsval  17561  qusval  17588  homfval  17736  comffval  17743  comfval  17744  oppccofval  17761  ismon  17780  sectfval  17798  invfval  17806  cofuval  17932  cofu2nd  17935  resfval  17942  isnat  18001  fucval  18013  fucco  18018  setchom  18133  setcco  18136  catchom  18156  catcco  18158  estrchom  18181  estrcco  18184  funcestrcsetclem5  18199  funcsetcestrclem5  18214  xpcval  18232  xpcid  18244  1stf2  18248  2ndf2  18251  prfval  18254  prf2fval  18256  evlfval  18273  evlf2  18274  evlf2val  18275  evlf1  18276  curfval  18279  uncfval  18290  diagval  18296  hof2fval  18311  hof2val  18312  yonedalem4a  18331  gsumvalx  18701  mgm2nsgrplem2  18944  mgm2nsgrplem3  18945  sgrp2nmndlem2  18949  sgrp2nmndlem3  18950  pwmndgplus  18960  symgov  19415  pj1fval  19726  rnghmval  20456  isrngim  20461  isrim0OLD  20497  isrim0  20499  rhmval  20516  rnghmsscmap2  20645  rnghmsscmap  20646  funcrngcsetc  20656  funcrngcsetcALT  20657  rhmsscmap2  20674  rhmsscmap  20675  funcringcsetc  20690  srhmsubclem3  20695  srhmsubc  20696  fldhmsubc  20802  rmodislmodlem  20943  rmodislmod  20944  rmodislmodOLD  20945  frlmphl  21818  uvcfval  21821  psrval  21952  selvffval  22154  psdffval  22178  mamufval  22411  mamuval  22412  mamufv  22413  matinvgcell  22456  mpomatmul  22467  mat1ov  22469  dmatval  22513  dmatmulcl  22521  scmatval  22525  scmatscmiddistr  22529  scmatscm  22534  mvmulfval  22563  mvmulval  22564  1mavmul  22569  maducoeval  22660  symgmatr01  22675  gsummatr01lem3  22678  gsummatr01lem4  22679  gsummatr01  22680  cpmat  22730  mat2pmatfval  22744  mat2pmatvalel  22746  mat2pmatmul  22752  cpm2mfval  22770  cpm2mvalel  22772  m2cpminvid  22774  m2cpminvid2  22776  decpmatval0  22785  decpmate  22787  decpmataa0  22789  decpmatmul  22793  pmatcollpw1  22797  monmatcollpw  22800  pmatcollpwlem  22801  pmatcollpw  22802  pmatcollpwscmatlem2  22811  pm2mpval  22816  pm2mpf1  22820  mptcoe1matfsupp  22823  mp2pm2mplem3  22829  mp2pm2mplem4  22830  chmatval  22850  chpmatfval  22851  chp0mat  22867  cnfval  23256  cnpfval  23257  fmval  23966  fmf  23968  fcfval  24056  tsmsval2  24153  blvalps  24410  blval  24411  ishtpy  25017  isphtpy  25026  rrxnm  25438  rrxmval  25452  rrxdsfival  25460  ehl2eudisval  25470  limcfval  25921  q1pval  26208  r1pval  26211  ismidb  28800  ttgitvval  28910  ebtwntg  29011  ecgrtg  29012  ewlksfval  29633  wwlksnon  29880  wspthsnon  29881  iswwlksnon  29882  iswspthsnon  29885  numclwlk1lem2  30398  ofoprabco  32680  of0r  32694  mntoval  32956  mgcoval  32960  elrgspnlem2  33232  rlocaddval  33254  rlocmulval  33255  idlsrgmulrval  33516  fedgmul  33658  smatfval  33755  lmatfval  33774  mdetpmtr1  33783  ofcfval  34078  sitmfval  34331  sseqval  34369  sseqf  34373  sseqp1  34376  cndprobval  34414  orvcval  34438  reprval  34603  lpadval  34669  satf  35337  satefv  35398  mclsval  35547  fwddifnval  36144  bj-imdirvallem  37162  finxpreclem1  37371  finxpreclem3  37375  ismtyval  37786  rrnmval  37814  isprimroot  42074  aks6d1c2p2  42100  aks6d1c2lem3  42107  aks6d1c2lem4  42108  aks6d1c6lem3  42153  ovmpogad  42254  tfsconcatun  43326  rfovd  43990  fsovd  43997  fsovrfovd  43998  mnringmulrvald  44222  bccval  44333  fmuldfeqlem1  45537  rrndistlt  46245  hoidmvval  46532  hspval  46564  hoiqssbllem2  46578  smflimlem3  46728  copissgrp  48011  copisnmnd  48012  intopval  48045  cznrng  48104  rngchomALTV  48111  rngccoALTV  48114  funcringcsetcALTV2lem5  48137  ringchomALTV  48145  ringccoALTV  48148  funcringcsetclem5ALTV  48160  srhmsubcALTVlem2  48167  srhmsubcALTV  48168  fldhmsubcALTV  48176  lmod1lem1  48332  lmod1lem2  48333  lmod1lem3  48334  lmod1lem4  48335  lmod1lem5  48336  fdivval  48388  digval  48447  itcoval1  48512  itcoval2  48513  itcoval3  48514  itcovalsucov  48517  ackvalsuc1mpt  48527  rrx2plordisom  48572  sphere  48596  functhinclem3  48842