Theorem ovmpod 7564

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  (class class class)co 7412   ∈ cmpo 7414

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6487  df-fun 6533  df-fv 6539  df-ov 7415  df-oprab 7416  df-mpo 7417

This theorem is used by:  ovmpoga  7566  fvmpopr2d  7574  elovmpod  7657  el2mpocsbcl  8085  fsplitfpar  8118  suppval  8163  sprmpod  8225  mpocurryd  8270  erov  8819  cnfcomlem  9684  swrdval  14771  pfxval  14803  splval  14880  0csh0  14924  relexp0g  15155  relexpsucnnr  15158  relexp1g  15159  ramval  17166  prdsval  17606  prdsplusgval  17624  prdsmulrval  17626  prdsdsval  17629  prdsvscaval  17630  imasval  17663  imasdsval  17667  qusval  17694  homfval  17846  comffval  17853  comfval  17854  oppccofval  17870  ismon  17888  sectfval  17906  invfval  17914  cofuval  18037  cofu2nd  18040  resfval  18047  isnat  18105  fucval  18116  fucco  18120  setchom  18235  setcco  18238  catchom  18258  catcco  18260  estrchom  18281  estrcco  18284  funcestrcsetclem5  18298  funcsetcestrclem5  18313  xpcval  18331  xpcid  18343  1stf2  18347  2ndf2  18350  prfval  18353  prf2fval  18355  evlfval  18371  evlf2  18372  evlf2val  18373  evlf1  18374  curfval  18377  uncfval  18388  diagval  18394  hof2fval  18409  hof2val  18410  yonedalem4a  18429  gsumvalx  18845  mgm2nsgrplem2  19098  mgm2nsgrplem3  19099  sgrp2nmndlem2  19103  sgrp2nmndlem3  19104  pwmndgplus  19121  symgov  19578  pj1fval  19888  rnghmval  20650  isrngim  20655  isrim0  20693  rhmval  20718  rnghmsscmap2  20861  rnghmsscmap  20862  funcrngcsetc  20872  funcrngcsetcALT  20873  rhmsscmap2  20890  rhmsscmap  20891  funcringcsetc  20906  srhmsubclem3  20911  srhmsubc  20912  fldhmsubc  21022  rmodislmodlem  21184  rmodislmod  21185  frlmphl  22067  uvcfval  22070  psrval  22203  selvffval  22407  psdffval  22458  mamufval  22687  mamuval  22688  mamufv  22689  matinvgcell  22730  mpomatmul  22741  mat1ov  22743  dmatval  22787  dmatmulcl  22795  scmatval  22799  scmatscmiddistr  22803  scmatscm  22808  mvmulfval  22837  mvmulval  22838  1mavmul  22843  maducoeval  22934  symgmatr01  22949  gsummatr01lem3  22952  gsummatr01lem4  22953  gsummatr01  22954  cpmat  23007  mat2pmatfval  23021  mat2pmatvalel  23023  mat2pmatmul  23029  cpm2mfval  23047  cpm2mvalel  23049  m2cpminvid  23051  m2cpminvid2  23053  decpmatval0  23062  decpmate  23064  decpmataa0  23066  decpmatmul  23070  pmatcollpw1  23074  monmatcollpw  23077  pmatcollpwlem  23078  pmatcollpw  23079  pmatcollpwscmatlem2  23088  pm2mpval  23093  pm2mpf1  23097  mptcoe1matfsupp  23100  mp2pm2mplem3  23106  mp2pm2mplem4  23107  chmatval  23127  chpmatfval  23128  chp0mat  23144  cnfval  23531  cnpfval  23532  fmval  24242  fmf  24244  fcfval  24332  tsmsval2  24429  blvalps  24684  blval  24685  ishtpy  25273  isphtpy  25282  rrxnm  25692  rrxmval  25706  rrxdsfival  25714  ehl2eudisval  25724  limcfval  26172  q1pval  26453  r1pval  26456  ismidb  29265  angmgmaddov1  29370  angmgmaddov2  29371  ttgitvval  29441  ebtwntg  29542  ecgrtg  29543  ewlksfval  30164  wwlksnon  30422  wspthsnon  30423  iswwlksnon  30424  iswspthsnon  30427  numclwlk1lem2  30953  ofoprabco  33240  of0r  33255  mntoval  33525  mgcoval  33529  fxpval  33708  conjga  33713  cntrval2  33714  elrgspnlem2  33786  rlocaddval  33812  rlocmulval  33813  idlsrgmulrval  34023  extvval  34145  mplvrpmfgalem  34158  mplvrpmga  34159  mplvrpmmhm  34160  mplvrpmrhm  34161  splyval  34173  issply  34175  esplyval  34176  fedgmul  34245  smatfval  34409  lmatfval  34428  mdetpmtr1  34437  ofcfval  34712  sitmfval  34965  sseqval  35003  sseqf  35007  sseqp1  35010  cndprobval  35048  orvcval  35073  reprval  35222  lpadval  35291  satf  36087  satefv  36148  mclsval  36297  fwddifnval  36898  bj-imdirvallem  38069  finxpreclem1  38280  finxpreclem3  38284  ismtyval  38702  rrnmval  38730  isprimroot  43111  aks6d1c2p2  43137  aks6d1c2lem3  43144  aks6d1c2lem4  43145  aks6d1c6lem3  43190  ovmpogad  43256  tfsconcatun  44297  rfovd  44960  fsovd  44967  fsovrfovd  44968  mnringmulrvald  45184  bccval  45281  fmuldfeqlem1  46538  rrndistlt  47244  hoidmvval  47531  hspval  47563  hoiqssbllem2  47577  smflimlem3  47727  copissgrp  49209  copisnmnd  49210  intopval  49243  cznrng  49302  rngchomALTV  49309  rngccoALTV  49312  funcringcsetcALTV2lem5  49335  ringchomALTV  49343  ringccoALTV  49346  funcringcsetclem5ALTV  49358  srhmsubcALTVlem2  49365  srhmsubcALTV  49366  fldhmsubcALTV  49374  lmod1lem1  49543  lmod1lem2  49544  lmod1lem3  49545  lmod1lem4  49546  lmod1lem5  49547  fdivval  49595  digval  49654  itcoval1  49719  itcoval2  49720  itcoval3  49721  itcovalsucov  49724  ackvalsuc1mpt  49734  rrx2plordisom  49779  sphere  49803  iinfssclem3  50108  swapfval  50314  swapf2vala  50322  fucofvalg  50370  fuco112x  50384  fuco21  50388  fuco22  50391  prcofvalg  50428  prcof2a  50441  prcof2  50442  opf2fval  50457  functhinclem3  50498  incat  50653  lanfval  50665  ranfval  50666  lanval  50671  ranval  50672  crosspdot0lem  50907