Theorem ovmpod 7498

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111  (class class class)co 7346   ∈ cmpo 7348

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3742  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-iota 6437  df-fun 6483  df-fv 6489  df-ov 7349  df-oprab 7350  df-mpo 7351

This theorem is referenced by:  ovmpoga  7500  fvmpopr2d  7508  elovmpod  7590  el2mpocsbcl  8015  fsplitfpar  8048  suppval  8092  sprmpod  8154  mpocurryd  8199  erov  8738  cnfcomlem  9589  swrdval  14548  pfxval  14578  splval  14655  0csh0  14697  relexp0g  14926  relexpsucnnr  14929  relexp1g  14930  ramval  16917  prdsval  17356  prdsplusgval  17374  prdsmulrval  17376  prdsdsval  17379  prdsvscaval  17380  imasval  17412  imasdsval  17416  qusval  17443  homfval  17595  comffval  17602  comfval  17603  oppccofval  17619  ismon  17637  sectfval  17655  invfval  17663  cofuval  17786  cofu2nd  17789  resfval  17796  isnat  17854  fucval  17865  fucco  17869  setchom  17984  setcco  17987  catchom  18007  catcco  18009  estrchom  18030  estrcco  18033  funcestrcsetclem5  18047  funcsetcestrclem5  18062  xpcval  18080  xpcid  18092  1stf2  18096  2ndf2  18099  prfval  18102  prf2fval  18104  evlfval  18120  evlf2  18121  evlf2val  18122  evlf1  18123  curfval  18126  uncfval  18137  diagval  18143  hof2fval  18158  hof2val  18159  yonedalem4a  18178  gsumvalx  18581  mgm2nsgrplem2  18824  mgm2nsgrplem3  18825  sgrp2nmndlem2  18829  sgrp2nmndlem3  18830  pwmndgplus  18840  symgov  19294  pj1fval  19604  rnghmval  20356  isrngim  20361  isrim0  20398  rhmval  20413  rnghmsscmap2  20542  rnghmsscmap  20543  funcrngcsetc  20553  funcrngcsetcALT  20554  rhmsscmap2  20571  rhmsscmap  20572  funcringcsetc  20587  srhmsubclem3  20592  srhmsubc  20593  fldhmsubc  20698  rmodislmodlem  20860  rmodislmod  20861  frlmphl  21716  uvcfval  21719  psrval  21850  selvffval  22046  psdffval  22070  mamufval  22305  mamuval  22306  mamufv  22307  matinvgcell  22348  mpomatmul  22359  mat1ov  22361  dmatval  22405  dmatmulcl  22413  scmatval  22417  scmatscmiddistr  22421  scmatscm  22426  mvmulfval  22455  mvmulval  22456  1mavmul  22461  maducoeval  22552  symgmatr01  22567  gsummatr01lem3  22570  gsummatr01lem4  22571  gsummatr01  22572  cpmat  22622  mat2pmatfval  22636  mat2pmatvalel  22638  mat2pmatmul  22644  cpm2mfval  22662  cpm2mvalel  22664  m2cpminvid  22666  m2cpminvid2  22668  decpmatval0  22677  decpmate  22679  decpmataa0  22681  decpmatmul  22685  pmatcollpw1  22689  monmatcollpw  22692  pmatcollpwlem  22693  pmatcollpw  22694  pmatcollpwscmatlem2  22703  pm2mpval  22708  pm2mpf1  22712  mptcoe1matfsupp  22715  mp2pm2mplem3  22721  mp2pm2mplem4  22722  chmatval  22742  chpmatfval  22743  chp0mat  22759  cnfval  23146  cnpfval  23147  fmval  23856  fmf  23858  fcfval  23946  tsmsval2  24043  blvalps  24298  blval  24299  ishtpy  24896  isphtpy  24905  rrxnm  25316  rrxmval  25330  rrxdsfival  25338  ehl2eudisval  25348  limcfval  25798  q1pval  26085  r1pval  26088  ismidb  28754  ttgitvval  28858  ebtwntg  28958  ecgrtg  28959  ewlksfval  29578  wwlksnon  29827  wspthsnon  29828  iswwlksnon  29829  iswspthsnon  29832  numclwlk1lem2  30345  ofoprabco  32641  of0r  32655  mntoval  32958  mgcoval  32962  fxpval  33129  conjga  33134  cntrval2  33135  elrgspnlem2  33205  rlocaddval  33230  rlocmulval  33231  idlsrgmulrval  33469  mplvrpmfgalem  33569  mplvrpmga  33570  mplvrpmmhm  33571  mplvrpmrhm  33572  splyval  33577  issply  33579  esplyval  33580  fedgmul  33639  smatfval  33803  lmatfval  33822  mdetpmtr1  33831  ofcfval  34106  sitmfval  34358  sseqval  34396  sseqf  34400  sseqp1  34403  cndprobval  34441  orvcval  34466  reprval  34618  lpadval  34684  satf  35385  satefv  35446  mclsval  35595  fwddifnval  36196  bj-imdirvallem  37213  finxpreclem1  37422  finxpreclem3  37426  ismtyval  37839  rrnmval  37867  isprimroot  42125  aks6d1c2p2  42151  aks6d1c2lem3  42158  aks6d1c2lem4  42159  aks6d1c6lem3  42204  ovmpogad  42267  tfsconcatun  43369  rfovd  44033  fsovd  44040  fsovrfovd  44041  mnringmulrvald  44259  bccval  44370  fmuldfeqlem1  45621  rrndistlt  46327  hoidmvval  46614  hspval  46646  hoiqssbllem2  46660  smflimlem3  46810  copissgrp  48198  copisnmnd  48199  intopval  48232  cznrng  48291  rngchomALTV  48298  rngccoALTV  48301  funcringcsetcALTV2lem5  48324  ringchomALTV  48332  ringccoALTV  48335  funcringcsetclem5ALTV  48347  srhmsubcALTVlem2  48354  srhmsubcALTV  48355  fldhmsubcALTV  48363  lmod1lem1  48518  lmod1lem2  48519  lmod1lem3  48520  lmod1lem4  48521  lmod1lem5  48522  fdivval  48570  digval  48629  itcoval1  48694  itcoval2  48695  itcoval3  48696  itcovalsucov  48699  ackvalsuc1mpt  48709  rrx2plordisom  48754  sphere  48778  iinfssclem3  49087  swapfval  49293  swapf2vala  49301  fucofvalg  49349  fuco112x  49363  fuco21  49367  fuco22  49370  prcofvalg  49407  prcof2a  49420  prcof2  49421  opf2fval  49436  functhinclem3  49477  incat  49632  lanfval  49644  ranfval  49645  lanval  49650  ranval  49651