Theorem ovmpod 7505

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  (class class class)co 7353   ∈ cmpo 7355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-sbc 3745  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-iota 6442  df-fun 6488  df-fv 6494  df-ov 7356  df-oprab 7357  df-mpo 7358

This theorem is referenced by:  ovmpoga  7507  fvmpopr2d  7515  elovmpod  7597  el2mpocsbcl  8025  fsplitfpar  8058  suppval  8102  sprmpod  8164  mpocurryd  8209  erov  8748  cnfcomlem  9614  swrdval  14568  pfxval  14598  splval  14675  0csh0  14717  relexp0g  14947  relexpsucnnr  14950  relexp1g  14951  ramval  16938  prdsval  17377  prdsplusgval  17395  prdsmulrval  17397  prdsdsval  17400  prdsvscaval  17401  imasval  17433  imasdsval  17437  qusval  17464  homfval  17616  comffval  17623  comfval  17624  oppccofval  17640  ismon  17658  sectfval  17676  invfval  17684  cofuval  17807  cofu2nd  17810  resfval  17817  isnat  17875  fucval  17886  fucco  17890  setchom  18005  setcco  18008  catchom  18028  catcco  18030  estrchom  18051  estrcco  18054  funcestrcsetclem5  18068  funcsetcestrclem5  18083  xpcval  18101  xpcid  18113  1stf2  18117  2ndf2  18120  prfval  18123  prf2fval  18125  evlfval  18141  evlf2  18142  evlf2val  18143  evlf1  18144  curfval  18147  uncfval  18158  diagval  18164  hof2fval  18179  hof2val  18180  yonedalem4a  18199  gsumvalx  18568  mgm2nsgrplem2  18811  mgm2nsgrplem3  18812  sgrp2nmndlem2  18816  sgrp2nmndlem3  18817  pwmndgplus  18827  symgov  19281  pj1fval  19591  rnghmval  20343  isrngim  20348  isrim0OLD  20384  isrim0  20386  rhmval  20403  rnghmsscmap2  20532  rnghmsscmap  20533  funcrngcsetc  20543  funcrngcsetcALT  20544  rhmsscmap2  20561  rhmsscmap  20562  funcringcsetc  20577  srhmsubclem3  20582  srhmsubc  20583  fldhmsubc  20688  rmodislmodlem  20850  rmodislmod  20851  frlmphl  21706  uvcfval  21709  psrval  21840  selvffval  22036  psdffval  22060  mamufval  22295  mamuval  22296  mamufv  22297  matinvgcell  22338  mpomatmul  22349  mat1ov  22351  dmatval  22395  dmatmulcl  22403  scmatval  22407  scmatscmiddistr  22411  scmatscm  22416  mvmulfval  22445  mvmulval  22446  1mavmul  22451  maducoeval  22542  symgmatr01  22557  gsummatr01lem3  22560  gsummatr01lem4  22561  gsummatr01  22562  cpmat  22612  mat2pmatfval  22626  mat2pmatvalel  22628  mat2pmatmul  22634  cpm2mfval  22652  cpm2mvalel  22654  m2cpminvid  22656  m2cpminvid2  22658  decpmatval0  22667  decpmate  22669  decpmataa0  22671  decpmatmul  22675  pmatcollpw1  22679  monmatcollpw  22682  pmatcollpwlem  22683  pmatcollpw  22684  pmatcollpwscmatlem2  22693  pm2mpval  22698  pm2mpf1  22702  mptcoe1matfsupp  22705  mp2pm2mplem3  22711  mp2pm2mplem4  22712  chmatval  22732  chpmatfval  22733  chp0mat  22749  cnfval  23136  cnpfval  23137  fmval  23846  fmf  23848  fcfval  23936  tsmsval2  24033  blvalps  24289  blval  24290  ishtpy  24887  isphtpy  24896  rrxnm  25307  rrxmval  25321  rrxdsfival  25329  ehl2eudisval  25339  limcfval  25789  q1pval  26076  r1pval  26079  ismidb  28741  ttgitvval  28845  ebtwntg  28945  ecgrtg  28946  ewlksfval  29565  wwlksnon  29814  wspthsnon  29815  iswwlksnon  29816  iswspthsnon  29819  numclwlk1lem2  30332  ofoprabco  32621  of0r  32635  mntoval  32937  mgcoval  32941  fxpval  33120  conjga  33125  cntrval2  33126  elrgspnlem2  33193  rlocaddval  33218  rlocmulval  33219  idlsrgmulrval  33456  fedgmul  33603  smatfval  33761  lmatfval  33780  mdetpmtr1  33789  ofcfval  34064  sitmfval  34317  sseqval  34355  sseqf  34359  sseqp1  34362  cndprobval  34400  orvcval  34425  reprval  34577  lpadval  34643  satf  35325  satefv  35386  mclsval  35535  fwddifnval  36136  bj-imdirvallem  37153  finxpreclem1  37362  finxpreclem3  37366  ismtyval  37779  rrnmval  37807  isprimroot  42066  aks6d1c2p2  42092  aks6d1c2lem3  42099  aks6d1c2lem4  42100  aks6d1c6lem3  42145  ovmpogad  42208  tfsconcatun  43310  rfovd  43974  fsovd  43981  fsovrfovd  43982  mnringmulrvald  44200  bccval  44311  fmuldfeqlem1  45564  rrndistlt  46272  hoidmvval  46559  hspval  46591  hoiqssbllem2  46605  smflimlem3  46755  copissgrp  48153  copisnmnd  48154  intopval  48187  cznrng  48246  rngchomALTV  48253  rngccoALTV  48256  funcringcsetcALTV2lem5  48279  ringchomALTV  48287  ringccoALTV  48290  funcringcsetclem5ALTV  48302  srhmsubcALTVlem2  48309  srhmsubcALTV  48310  fldhmsubcALTV  48318  lmod1lem1  48473  lmod1lem2  48474  lmod1lem3  48475  lmod1lem4  48476  lmod1lem5  48477  fdivval  48525  digval  48584  itcoval1  48649  itcoval2  48650  itcoval3  48651  itcovalsucov  48654  ackvalsuc1mpt  48664  rrx2plordisom  48709  sphere  48733  iinfssclem3  49042  swapfval  49248  swapf2vala  49256  fucofvalg  49304  fuco112x  49318  fuco21  49322  fuco22  49325  prcofvalg  49362  prcof2a  49375  prcof2  49376  opf2fval  49391  functhinclem3  49432  incat  49587  lanfval  49599  ranfval  49600  lanval  49605  ranval  49606