Theorem ovmpod 7520

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  (class class class)co 7368   ∈ cmpo 7370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-iota 6456  df-fun 6502  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373

This theorem is referenced by:  ovmpoga  7522  fvmpopr2d  7530  elovmpod  7612  el2mpocsbcl  8037  fsplitfpar  8070  suppval  8114  sprmpod  8176  mpocurryd  8221  erov  8763  cnfcomlem  9620  swrdval  14579  pfxval  14609  splval  14686  0csh0  14728  relexp0g  14957  relexpsucnnr  14960  relexp1g  14961  ramval  16948  prdsval  17387  prdsplusgval  17405  prdsmulrval  17407  prdsdsval  17410  prdsvscaval  17411  imasval  17444  imasdsval  17448  qusval  17475  homfval  17627  comffval  17634  comfval  17635  oppccofval  17651  ismon  17669  sectfval  17687  invfval  17695  cofuval  17818  cofu2nd  17821  resfval  17828  isnat  17886  fucval  17897  fucco  17901  setchom  18016  setcco  18019  catchom  18039  catcco  18041  estrchom  18062  estrcco  18065  funcestrcsetclem5  18079  funcsetcestrclem5  18094  xpcval  18112  xpcid  18124  1stf2  18128  2ndf2  18131  prfval  18134  prf2fval  18136  evlfval  18152  evlf2  18153  evlf2val  18154  evlf1  18155  curfval  18158  uncfval  18169  diagval  18175  hof2fval  18190  hof2val  18191  yonedalem4a  18210  gsumvalx  18613  mgm2nsgrplem2  18856  mgm2nsgrplem3  18857  sgrp2nmndlem2  18861  sgrp2nmndlem3  18862  pwmndgplus  18872  symgov  19325  pj1fval  19635  rnghmval  20388  isrngim  20393  isrim0  20430  rhmval  20445  rnghmsscmap2  20574  rnghmsscmap  20575  funcrngcsetc  20585  funcrngcsetcALT  20586  rhmsscmap2  20603  rhmsscmap  20604  funcringcsetc  20619  srhmsubclem3  20624  srhmsubc  20625  fldhmsubc  20730  rmodislmodlem  20892  rmodislmod  20893  frlmphl  21748  uvcfval  21751  psrval  21883  selvffval  22088  psdffval  22112  mamufval  22348  mamuval  22349  mamufv  22350  matinvgcell  22391  mpomatmul  22402  mat1ov  22404  dmatval  22448  dmatmulcl  22456  scmatval  22460  scmatscmiddistr  22464  scmatscm  22469  mvmulfval  22498  mvmulval  22499  1mavmul  22504  maducoeval  22595  symgmatr01  22610  gsummatr01lem3  22613  gsummatr01lem4  22614  gsummatr01  22615  cpmat  22665  mat2pmatfval  22679  mat2pmatvalel  22681  mat2pmatmul  22687  cpm2mfval  22705  cpm2mvalel  22707  m2cpminvid  22709  m2cpminvid2  22711  decpmatval0  22720  decpmate  22722  decpmataa0  22724  decpmatmul  22728  pmatcollpw1  22732  monmatcollpw  22735  pmatcollpwlem  22736  pmatcollpw  22737  pmatcollpwscmatlem2  22746  pm2mpval  22751  pm2mpf1  22755  mptcoe1matfsupp  22758  mp2pm2mplem3  22764  mp2pm2mplem4  22765  chmatval  22785  chpmatfval  22786  chp0mat  22802  cnfval  23189  cnpfval  23190  fmval  23899  fmf  23901  fcfval  23989  tsmsval2  24086  blvalps  24341  blval  24342  ishtpy  24939  isphtpy  24948  rrxnm  25359  rrxmval  25373  rrxdsfival  25381  ehl2eudisval  25391  limcfval  25841  q1pval  26128  r1pval  26131  ismidb  28862  ttgitvval  28966  ebtwntg  29067  ecgrtg  29068  ewlksfval  29687  wwlksnon  29936  wspthsnon  29937  iswwlksnon  29938  iswspthsnon  29941  numclwlk1lem2  30457  ofoprabco  32753  of0r  32768  mntoval  33074  mgcoval  33078  fxpval  33258  conjga  33263  cntrval2  33264  elrgspnlem2  33336  rlocaddval  33361  rlocmulval  33362  idlsrgmulrval  33601  extvval  33707  mplvrpmfgalem  33720  mplvrpmga  33721  mplvrpmmhm  33722  mplvrpmrhm  33723  splyval  33735  issply  33737  esplyval  33738  fedgmul  33808  smatfval  33972  lmatfval  33991  mdetpmtr1  34000  ofcfval  34275  sitmfval  34527  sseqval  34565  sseqf  34569  sseqp1  34572  cndprobval  34610  orvcval  34635  reprval  34787  lpadval  34853  satf  35566  satefv  35627  mclsval  35776  fwddifnval  36376  bj-imdirvallem  37429  finxpreclem1  37638  finxpreclem3  37642  ismtyval  38045  rrnmval  38073  isprimroot  42457  aks6d1c2p2  42483  aks6d1c2lem3  42490  aks6d1c2lem4  42491  aks6d1c6lem3  42536  ovmpogad  42601  tfsconcatun  43688  rfovd  44351  fsovd  44358  fsovrfovd  44359  mnringmulrvald  44577  bccval  44688  fmuldfeqlem1  45936  rrndistlt  46642  hoidmvval  46929  hspval  46961  hoiqssbllem2  46975  smflimlem3  47125  copissgrp  48522  copisnmnd  48523  intopval  48556  cznrng  48615  rngchomALTV  48622  rngccoALTV  48625  funcringcsetcALTV2lem5  48648  ringchomALTV  48656  ringccoALTV  48659  funcringcsetclem5ALTV  48671  srhmsubcALTVlem2  48678  srhmsubcALTV  48679  fldhmsubcALTV  48687  lmod1lem1  48841  lmod1lem2  48842  lmod1lem3  48843  lmod1lem4  48844  lmod1lem5  48845  fdivval  48893  digval  48952  itcoval1  49017  itcoval2  49018  itcoval3  49019  itcovalsucov  49022  ackvalsuc1mpt  49032  rrx2plordisom  49077  sphere  49101  iinfssclem3  49409  swapfval  49615  swapf2vala  49623  fucofvalg  49671  fuco112x  49685  fuco21  49689  fuco22  49692  prcofvalg  49729  prcof2a  49742  prcof2  49743  opf2fval  49758  functhinclem3  49799  incat  49954  lanfval  49966  ranfval  49967  lanval  49972  ranval  49973