Theorem ovmpod 7515

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 7514	1 ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  (class class class)co 7363   ∈ cmpo 7365

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-iota 6448  df-fun 6494  df-fv 6500  df-ov 7366  df-oprab 7367  df-mpo 7368

This theorem is referenced by:  ovmpoga  7517  fvmpopr2d  7525  elovmpod  7607  el2mpocsbcl  8031  fsplitfpar  8064  suppval  8109  sprmpod  8171  mpocurryd  8216  erov  8758  cnfcomlem  9618  swrdval  14604  pfxval  14634  splval  14711  0csh0  14753  relexp0g  14982  relexpsucnnr  14985  relexp1g  14986  ramval  16977  prdsval  17416  prdsplusgval  17434  prdsmulrval  17436  prdsdsval  17439  prdsvscaval  17440  imasval  17473  imasdsval  17477  qusval  17504  homfval  17656  comffval  17663  comfval  17664  oppccofval  17680  ismon  17698  sectfval  17716  invfval  17724  cofuval  17847  cofu2nd  17850  resfval  17857  isnat  17915  fucval  17926  fucco  17930  setchom  18045  setcco  18048  catchom  18068  catcco  18070  estrchom  18091  estrcco  18094  funcestrcsetclem5  18108  funcsetcestrclem5  18123  xpcval  18141  xpcid  18153  1stf2  18157  2ndf2  18160  prfval  18163  prf2fval  18165  evlfval  18181  evlf2  18182  evlf2val  18183  evlf1  18184  curfval  18187  uncfval  18198  diagval  18204  hof2fval  18219  hof2val  18220  yonedalem4a  18239  gsumvalx  18642  mgm2nsgrplem2  18888  mgm2nsgrplem3  18889  sgrp2nmndlem2  18893  sgrp2nmndlem3  18894  pwmndgplus  18904  symgov  19357  pj1fval  19667  rnghmval  20418  isrngim  20423  isrim0  20460  rhmval  20478  rnghmsscmap2  20608  rnghmsscmap  20609  funcrngcsetc  20619  funcrngcsetcALT  20620  rhmsscmap2  20637  rhmsscmap  20638  funcringcsetc  20653  srhmsubclem3  20658  srhmsubc  20659  fldhmsubc  20764  rmodislmodlem  20926  rmodislmod  20927  frlmphl  21763  uvcfval  21766  psrval  21897  selvffval  22101  psdffval  22152  mamufval  22382  mamuval  22383  mamufv  22384  matinvgcell  22425  mpomatmul  22436  mat1ov  22438  dmatval  22482  dmatmulcl  22490  scmatval  22494  scmatscmiddistr  22498  scmatscm  22503  mvmulfval  22532  mvmulval  22533  1mavmul  22538  maducoeval  22629  symgmatr01  22644  gsummatr01lem3  22647  gsummatr01lem4  22648  gsummatr01  22649  cpmat  22699  mat2pmatfval  22713  mat2pmatvalel  22715  mat2pmatmul  22721  cpm2mfval  22739  cpm2mvalel  22741  m2cpminvid  22743  m2cpminvid2  22745  decpmatval0  22754  decpmate  22756  decpmataa0  22758  decpmatmul  22762  pmatcollpw1  22766  monmatcollpw  22769  pmatcollpwlem  22770  pmatcollpw  22771  pmatcollpwscmatlem2  22780  pm2mpval  22785  pm2mpf1  22789  mptcoe1matfsupp  22792  mp2pm2mplem3  22798  mp2pm2mplem4  22799  chmatval  22819  chpmatfval  22820  chp0mat  22836  cnfval  23223  cnpfval  23224  fmval  23933  fmf  23935  fcfval  24023  tsmsval2  24120  blvalps  24375  blval  24376  ishtpy  24964  isphtpy  24973  rrxnm  25383  rrxmval  25397  rrxdsfival  25405  ehl2eudisval  25415  limcfval  25864  q1pval  26145  r1pval  26148  ismidb  28871  ttgitvval  28975  ebtwntg  29076  ecgrtg  29077  ewlksfval  29695  wwlksnon  29944  wspthsnon  29945  iswwlksnon  29946  iswspthsnon  29949  numclwlk1lem2  30465  ofoprabco  32763  of0r  32778  mntoval  33068  mgcoval  33072  fxpval  33253  conjga  33258  cntrval2  33259  elrgspnlem2  33331  rlocaddval  33356  rlocmulval  33357  idlsrgmulrval  33599  extvval  33722  mplvrpmfgalem  33735  mplvrpmga  33736  mplvrpmmhm  33737  mplvrpmrhm  33738  splyval  33750  issply  33752  esplyval  33753  fedgmul  33822  smatfval  33986  lmatfval  34005  mdetpmtr1  34014  ofcfval  34289  sitmfval  34541  sseqval  34579  sseqf  34583  sseqp1  34586  cndprobval  34624  orvcval  34649  reprval  34801  lpadval  34867  satf  35588  satefv  35649  mclsval  35798  fwddifnval  36398  bj-imdirvallem  37547  finxpreclem1  37758  finxpreclem3  37762  ismtyval  38174  rrnmval  38202  isprimroot  42585  aks6d1c2p2  42611  aks6d1c2lem3  42618  aks6d1c2lem4  42619  aks6d1c6lem3  42664  ovmpogad  42728  tfsconcatun  43789  rfovd  44452  fsovd  44459  fsovrfovd  44460  mnringmulrvald  44678  bccval  44789  fmuldfeqlem1  46034  rrndistlt  46740  hoidmvval  47027  hspval  47059  hoiqssbllem2  47073  smflimlem3  47223  copissgrp  48666  copisnmnd  48667  intopval  48700  cznrng  48759  rngchomALTV  48766  rngccoALTV  48769  funcringcsetcALTV2lem5  48792  ringchomALTV  48800  ringccoALTV  48803  funcringcsetclem5ALTV  48815  srhmsubcALTVlem2  48822  srhmsubcALTV  48823  fldhmsubcALTV  48831  lmod1lem1  48985  lmod1lem2  48986  lmod1lem3  48987  lmod1lem4  48988  lmod1lem5  48989  fdivval  49037  digval  49096  itcoval1  49161  itcoval2  49162  itcoval3  49163  itcovalsucov  49166  ackvalsuc1mpt  49176  rrx2plordisom  49221  sphere  49245  iinfssclem3  49553  swapfval  49759  swapf2vala  49767  fucofvalg  49815  fuco112x  49829  fuco21  49833  fuco22  49836  prcofvalg  49873  prcof2a  49886  prcof2  49887  opf2fval  49902  functhinclem3  49943  incat  50098  lanfval  50110  ranfval  50111  lanval  50116  ranval  50117