Theorem ovmpod 7568

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  (class class class)co 7416   ∈ cmpo 7418

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5260  ax-pr 5407

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 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-sbc 3748  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4491  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4876  df-br 5113  df-opab 5177  df-id 5559  df-xp 5670  df-rel 5671  df-cnv 5672  df-co 5673  df-dm 5674  df-iota 6496  df-fun 6542  df-fv 6548  df-ov 7419  df-oprab 7420  df-mpo 7421

This theorem is used by:  ovmpoga  7570  fvmpopr2d  7578  elovmpod  7660  el2mpocsbcl  8082  fsplitfpar  8115  suppval  8160  sprmpod  8222  mpocurryd  8267  erov  8814  cnfcomlem  9670  swrdval  14692  pfxval  14722  splval  14799  0csh0  14841  relexp0g  15070  relexpsucnnr  15073  relexp1g  15074  ramval  17078  prdsval  17518  prdsplusgval  17536  prdsmulrval  17538  prdsdsval  17541  prdsvscaval  17542  imasval  17575  imasdsval  17579  qusval  17606  homfval  17758  comffval  17765  comfval  17766  oppccofval  17782  ismon  17800  sectfval  17818  invfval  17826  cofuval  17949  cofu2nd  17952  resfval  17959  isnat  18017  fucval  18028  fucco  18032  setchom  18147  setcco  18150  catchom  18170  catcco  18172  estrchom  18193  estrcco  18196  funcestrcsetclem5  18210  funcsetcestrclem5  18225  xpcval  18243  xpcid  18255  1stf2  18259  2ndf2  18262  prfval  18265  prf2fval  18267  evlfval  18283  evlf2  18284  evlf2val  18285  evlf1  18286  curfval  18289  uncfval  18300  diagval  18306  hof2fval  18321  hof2val  18322  yonedalem4a  18341  gsumvalx  18744  mgm2nsgrplem2  18991  mgm2nsgrplem3  18992  sgrp2nmndlem2  18996  sgrp2nmndlem3  18997  pwmndgplus  19007  symgov  19464  pj1fval  19774  rnghmval  20533  isrngim  20538  isrim0  20576  rhmval  20601  rnghmsscmap2  20743  rnghmsscmap  20744  funcrngcsetc  20754  funcrngcsetcALT  20755  rhmsscmap2  20772  rhmsscmap  20773  funcringcsetc  20788  srhmsubclem3  20793  srhmsubc  20794  fldhmsubc  20903  rmodislmodlem  21065  rmodislmod  21066  frlmphl  21946  uvcfval  21949  psrval  22080  selvffval  22284  psdffval  22335  mamufval  22564  mamuval  22565  mamufv  22566  matinvgcell  22607  mpomatmul  22618  mat1ov  22620  dmatval  22664  dmatmulcl  22672  scmatval  22676  scmatscmiddistr  22680  scmatscm  22685  mvmulfval  22714  mvmulval  22715  1mavmul  22720  maducoeval  22811  symgmatr01  22826  gsummatr01lem3  22829  gsummatr01lem4  22830  gsummatr01  22831  cpmat  22881  mat2pmatfval  22895  mat2pmatvalel  22897  mat2pmatmul  22903  cpm2mfval  22921  cpm2mvalel  22923  m2cpminvid  22925  m2cpminvid2  22927  decpmatval0  22936  decpmate  22938  decpmataa0  22940  decpmatmul  22944  pmatcollpw1  22948  monmatcollpw  22951  pmatcollpwlem  22952  pmatcollpw  22953  pmatcollpwscmatlem2  22962  pm2mpval  22967  pm2mpf1  22971  mptcoe1matfsupp  22974  mp2pm2mplem3  22980  mp2pm2mplem4  22981  chmatval  23001  chpmatfval  23002  chp0mat  23018  cnfval  23405  cnpfval  23406  fmval  24115  fmf  24117  fcfval  24205  tsmsval2  24302  blvalps  24557  blval  24558  ishtpy  25146  isphtpy  25155  rrxnm  25565  rrxmval  25579  rrxdsfival  25587  ehl2eudisval  25597  limcfval  26046  q1pval  26327  r1pval  26330  ismidb  29102  ttgitvval  29246  ebtwntg  29347  ecgrtg  29348  ewlksfval  29966  wwlksnon  30215  wspthsnon  30216  iswwlksnon  30217  iswspthsnon  30220  numclwlk1lem2  30736  ofoprabco  33024  of0r  33039  mntoval  33315  mgcoval  33319  fxpval  33498  conjga  33503  cntrval2  33504  elrgspnlem2  33576  rlocaddval  33602  rlocmulval  33603  idlsrgmulrval  33812  extvval  33934  mplvrpmfgalem  33947  mplvrpmga  33948  mplvrpmmhm  33949  mplvrpmrhm  33950  splyval  33962  issply  33964  esplyval  33965  fedgmul  34034  smatfval  34198  lmatfval  34217  mdetpmtr1  34226  ofcfval  34501  sitmfval  34753  sseqval  34791  sseqf  34795  sseqp1  34798  cndprobval  34836  orvcval  34861  reprval  35010  lpadval  35079  satf  35857  satefv  35918  mclsval  36067  fwddifnval  36667  bj-imdirvallem  37856  finxpreclem1  38067  finxpreclem3  38071  ismtyval  38483  rrnmval  38511  isprimroot  42892  aks6d1c2p2  42918  aks6d1c2lem3  42925  aks6d1c2lem4  42926  aks6d1c6lem3  42971  ovmpogad  43037  tfsconcatun  44096  rfovd  44759  fsovd  44766  fsovrfovd  44767  mnringmulrvald  44983  bccval  45080  fmuldfeqlem1  46330  rrndistlt  47036  hoidmvval  47323  hspval  47355  hoiqssbllem2  47369  smflimlem3  47519  copissgrp  48965  copisnmnd  48966  intopval  48999  cznrng  49058  rngchomALTV  49065  rngccoALTV  49068  funcringcsetcALTV2lem5  49091  ringchomALTV  49099  ringccoALTV  49102  funcringcsetclem5ALTV  49114  srhmsubcALTVlem2  49121  srhmsubcALTV  49122  fldhmsubcALTV  49130  lmod1lem1  49299  lmod1lem2  49300  lmod1lem3  49301  lmod1lem4  49302  lmod1lem5  49303  fdivval  49351  digval  49410  itcoval1  49475  itcoval2  49476  itcoval3  49477  itcovalsucov  49480  ackvalsuc1mpt  49490  rrx2plordisom  49535  sphere  49559  iinfssclem3  49866  swapfval  50072  swapf2vala  50080  fucofvalg  50128  fuco112x  50142  fuco21  50146  fuco22  50149  prcofvalg  50186  prcof2a  50199  prcof2  50200  opf2fval  50215  functhinclem3  50256  incat  50411  lanfval  50423  ranfval  50424  lanval  50429  ranval  50430  crosspdot0i  50676