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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  (class class class)co 7412   ∈ cmpo 7414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3746  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-iota 6494  df-fun 6540  df-fv 6546  df-ov 7415  df-oprab 7416  df-mpo 7417

This theorem is referenced by:  ovmpoga  7566  fvmpopr2d  7574  elovmpod  7656  el2mpocsbcl  8081  fsplitfpar  8114  suppval  8159  sprmpod  8221  mpocurryd  8266  erov  8813  cnfcomlem  9669  swrdval  14683  pfxval  14713  splval  14790  0csh0  14832  relexp0g  15061  relexpsucnnr  15064  relexp1g  15065  ramval  17069  prdsval  17509  prdsplusgval  17527  prdsmulrval  17529  prdsdsval  17532  prdsvscaval  17533  imasval  17566  imasdsval  17570  qusval  17597  homfval  17749  comffval  17756  comfval  17757  oppccofval  17773  ismon  17791  sectfval  17809  invfval  17817  cofuval  17940  cofu2nd  17943  resfval  17950  isnat  18008  fucval  18019  fucco  18023  setchom  18138  setcco  18141  catchom  18161  catcco  18163  estrchom  18184  estrcco  18187  funcestrcsetclem5  18201  funcsetcestrclem5  18216  xpcval  18234  xpcid  18246  1stf2  18250  2ndf2  18253  prfval  18256  prf2fval  18258  evlfval  18274  evlf2  18275  evlf2val  18276  evlf1  18277  curfval  18280  uncfval  18291  diagval  18297  hof2fval  18312  hof2val  18313  yonedalem4a  18332  gsumvalx  18735  mgm2nsgrplem2  18982  mgm2nsgrplem3  18983  sgrp2nmndlem2  18987  sgrp2nmndlem3  18988  pwmndgplus  18998  symgov  19455  pj1fval  19765  rnghmval  20523  isrngim  20528  isrim0  20565  rhmval  20583  rnghmsscmap2  20715  rnghmsscmap  20716  funcrngcsetc  20726  funcrngcsetcALT  20727  rhmsscmap2  20744  rhmsscmap  20745  funcringcsetc  20760  srhmsubclem3  20765  srhmsubc  20766  fldhmsubc  20869  rmodislmodlem  21031  rmodislmod  21032  frlmphl  21912  uvcfval  21915  psrval  22046  selvffval  22250  psdffval  22301  mamufval  22530  mamuval  22531  mamufv  22532  matinvgcell  22573  mpomatmul  22584  mat1ov  22586  dmatval  22630  dmatmulcl  22638  scmatval  22642  scmatscmiddistr  22646  scmatscm  22651  mvmulfval  22680  mvmulval  22681  1mavmul  22686  maducoeval  22777  symgmatr01  22792  gsummatr01lem3  22795  gsummatr01lem4  22796  gsummatr01  22797  cpmat  22847  mat2pmatfval  22861  mat2pmatvalel  22863  mat2pmatmul  22869  cpm2mfval  22887  cpm2mvalel  22889  m2cpminvid  22891  m2cpminvid2  22893  decpmatval0  22902  decpmate  22904  decpmataa0  22906  decpmatmul  22910  pmatcollpw1  22914  monmatcollpw  22917  pmatcollpwlem  22918  pmatcollpw  22919  pmatcollpwscmatlem2  22928  pm2mpval  22933  pm2mpf1  22937  mptcoe1matfsupp  22940  mp2pm2mplem3  22946  mp2pm2mplem4  22947  chmatval  22967  chpmatfval  22968  chp0mat  22984  cnfval  23371  cnpfval  23372  fmval  24081  fmf  24083  fcfval  24171  tsmsval2  24268  blvalps  24523  blval  24524  ishtpy  25112  isphtpy  25121  rrxnm  25531  rrxmval  25545  rrxdsfival  25553  ehl2eudisval  25563  limcfval  26012  q1pval  26293  r1pval  26296  ismidb  29065  ttgitvval  29209  ebtwntg  29310  ecgrtg  29311  ewlksfval  29929  wwlksnon  30178  wspthsnon  30179  iswwlksnon  30180  iswspthsnon  30183  numclwlk1lem2  30699  ofoprabco  32987  of0r  33002  mntoval  33280  mgcoval  33284  fxpval  33463  conjga  33468  cntrval2  33469  elrgspnlem2  33541  rlocaddval  33567  rlocmulval  33568  idlsrgmulrval  33777  extvval  33899  mplvrpmfgalem  33912  mplvrpmga  33913  mplvrpmmhm  33914  mplvrpmrhm  33915  splyval  33927  issply  33929  esplyval  33930  fedgmul  33999  smatfval  34163  lmatfval  34182  mdetpmtr1  34191  ofcfval  34466  sitmfval  34718  sseqval  34756  sseqf  34760  sseqp1  34763  cndprobval  34801  orvcval  34826  reprval  34975  lpadval  35044  satf  35823  satefv  35884  mclsval  36033  fwddifnval  36633  bj-imdirvallem  37802  finxpreclem1  38013  finxpreclem3  38017  ismtyval  38429  rrnmval  38457  isprimroot  42838  aks6d1c2p2  42864  aks6d1c2lem3  42871  aks6d1c2lem4  42872  aks6d1c6lem3  42917  ovmpogad  42983  tfsconcatun  44044  rfovd  44707  fsovd  44714  fsovrfovd  44715  mnringmulrvald  44931  bccval  45028  fmuldfeqlem1  46278  rrndistlt  46984  hoidmvval  47271  hspval  47303  hoiqssbllem2  47317  smflimlem3  47467  copissgrp  48910  copisnmnd  48911  intopval  48944  cznrng  49003  rngchomALTV  49010  rngccoALTV  49013  funcringcsetcALTV2lem5  49036  ringchomALTV  49044  ringccoALTV  49047  funcringcsetclem5ALTV  49059  srhmsubcALTVlem2  49066  srhmsubcALTV  49067  fldhmsubcALTV  49075  lmod1lem1  49244  lmod1lem2  49245  lmod1lem3  49246  lmod1lem4  49247  lmod1lem5  49248  fdivval  49296  digval  49355  itcoval1  49420  itcoval2  49421  itcoval3  49422  itcovalsucov  49425  ackvalsuc1mpt  49435  rrx2plordisom  49480  sphere  49504  iinfssclem3  49811  swapfval  50017  swapf2vala  50025  fucofvalg  50073  fuco112x  50087  fuco21  50091  fuco22  50094  prcofvalg  50131  prcof2a  50144  prcof2  50145  opf2fval  50160  functhinclem3  50201  incat  50356  lanfval  50368  ranfval  50369  lanval  50374  ranval  50375