Theorem ovmpod 7504

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  (class class class)co 7352   ∈ cmpo 7354

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372

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 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-sbc 3738  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-iota 6442  df-fun 6488  df-fv 6494  df-ov 7355  df-oprab 7356  df-mpo 7357

This theorem is referenced by:  ovmpoga  7506  fvmpopr2d  7514  elovmpod  7596  el2mpocsbcl  8021  fsplitfpar  8054  suppval  8098  sprmpod  8160  mpocurryd  8205  erov  8744  cnfcomlem  9596  swrdval  14553  pfxval  14583  splval  14660  0csh0  14702  relexp0g  14931  relexpsucnnr  14934  relexp1g  14935  ramval  16922  prdsval  17361  prdsplusgval  17379  prdsmulrval  17381  prdsdsval  17384  prdsvscaval  17385  imasval  17417  imasdsval  17421  qusval  17448  homfval  17600  comffval  17607  comfval  17608  oppccofval  17624  ismon  17642  sectfval  17660  invfval  17668  cofuval  17791  cofu2nd  17794  resfval  17801  isnat  17859  fucval  17870  fucco  17874  setchom  17989  setcco  17992  catchom  18012  catcco  18014  estrchom  18035  estrcco  18038  funcestrcsetclem5  18052  funcsetcestrclem5  18067  xpcval  18085  xpcid  18097  1stf2  18101  2ndf2  18104  prfval  18107  prf2fval  18109  evlfval  18125  evlf2  18126  evlf2val  18127  evlf1  18128  curfval  18131  uncfval  18142  diagval  18148  hof2fval  18163  hof2val  18164  yonedalem4a  18183  gsumvalx  18586  mgm2nsgrplem2  18829  mgm2nsgrplem3  18830  sgrp2nmndlem2  18834  sgrp2nmndlem3  18835  pwmndgplus  18845  symgov  19298  pj1fval  19608  rnghmval  20360  isrngim  20365  isrim0  20402  rhmval  20417  rnghmsscmap2  20546  rnghmsscmap  20547  funcrngcsetc  20557  funcrngcsetcALT  20558  rhmsscmap2  20575  rhmsscmap  20576  funcringcsetc  20591  srhmsubclem3  20596  srhmsubc  20597  fldhmsubc  20702  rmodislmodlem  20864  rmodislmod  20865  frlmphl  21720  uvcfval  21723  psrval  21854  selvffval  22049  psdffval  22073  mamufval  22308  mamuval  22309  mamufv  22310  matinvgcell  22351  mpomatmul  22362  mat1ov  22364  dmatval  22408  dmatmulcl  22416  scmatval  22420  scmatscmiddistr  22424  scmatscm  22429  mvmulfval  22458  mvmulval  22459  1mavmul  22464  maducoeval  22555  symgmatr01  22570  gsummatr01lem3  22573  gsummatr01lem4  22574  gsummatr01  22575  cpmat  22625  mat2pmatfval  22639  mat2pmatvalel  22641  mat2pmatmul  22647  cpm2mfval  22665  cpm2mvalel  22667  m2cpminvid  22669  m2cpminvid2  22671  decpmatval0  22680  decpmate  22682  decpmataa0  22684  decpmatmul  22688  pmatcollpw1  22692  monmatcollpw  22695  pmatcollpwlem  22696  pmatcollpw  22697  pmatcollpwscmatlem2  22706  pm2mpval  22711  pm2mpf1  22715  mptcoe1matfsupp  22718  mp2pm2mplem3  22724  mp2pm2mplem4  22725  chmatval  22745  chpmatfval  22746  chp0mat  22762  cnfval  23149  cnpfval  23150  fmval  23859  fmf  23861  fcfval  23949  tsmsval2  24046  blvalps  24301  blval  24302  ishtpy  24899  isphtpy  24908  rrxnm  25319  rrxmval  25333  rrxdsfival  25341  ehl2eudisval  25351  limcfval  25801  q1pval  26088  r1pval  26091  ismidb  28757  ttgitvval  28861  ebtwntg  28962  ecgrtg  28963  ewlksfval  29582  wwlksnon  29831  wspthsnon  29832  iswwlksnon  29833  iswspthsnon  29836  numclwlk1lem2  30352  ofoprabco  32648  of0r  32664  mntoval  32970  mgcoval  32974  fxpval  33141  conjga  33146  cntrval2  33147  elrgspnlem2  33217  rlocaddval  33242  rlocmulval  33243  idlsrgmulrval  33481  extvval  33582  mplvrpmfgalem  33592  mplvrpmga  33593  mplvrpmmhm  33594  mplvrpmrhm  33595  splyval  33600  issply  33602  esplyval  33603  fedgmul  33665  smatfval  33829  lmatfval  33848  mdetpmtr1  33857  ofcfval  34132  sitmfval  34384  sseqval  34422  sseqf  34426  sseqp1  34429  cndprobval  34467  orvcval  34492  reprval  34644  lpadval  34710  satf  35418  satefv  35479  mclsval  35628  fwddifnval  36228  bj-imdirvallem  37245  finxpreclem1  37454  finxpreclem3  37458  ismtyval  37861  rrnmval  37889  isprimroot  42207  aks6d1c2p2  42233  aks6d1c2lem3  42240  aks6d1c2lem4  42241  aks6d1c6lem3  42286  ovmpogad  42354  tfsconcatun  43455  rfovd  44119  fsovd  44126  fsovrfovd  44127  mnringmulrvald  44345  bccval  44456  fmuldfeqlem1  45707  rrndistlt  46413  hoidmvval  46700  hspval  46732  hoiqssbllem2  46746  smflimlem3  46896  copissgrp  48293  copisnmnd  48294  intopval  48327  cznrng  48386  rngchomALTV  48393  rngccoALTV  48396  funcringcsetcALTV2lem5  48419  ringchomALTV  48427  ringccoALTV  48430  funcringcsetclem5ALTV  48442  srhmsubcALTVlem2  48449  srhmsubcALTV  48450  fldhmsubcALTV  48458  lmod1lem1  48613  lmod1lem2  48614  lmod1lem3  48615  lmod1lem4  48616  lmod1lem5  48617  fdivval  48665  digval  48724  itcoval1  48789  itcoval2  48790  itcoval3  48791  itcovalsucov  48794  ackvalsuc1mpt  48804  rrx2plordisom  48849  sphere  48873  iinfssclem3  49182  swapfval  49388  swapf2vala  49396  fucofvalg  49444  fuco112x  49458  fuco21  49462  fuco22  49465  prcofvalg  49502  prcof2a  49515  prcof2  49516  opf2fval  49531  functhinclem3  49572  incat  49727  lanfval  49739  ranfval  49740  lanval  49745  ranval  49746