Theorem ovmpod 7165

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1525   ∈ wcel 2083  (class class class)co 7023   ∈ cmpo 7025

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-sep 5101  ax-nul 5108  ax-pr 5228

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3442  df-sbc 3712  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-if 4388  df-sn 4479  df-pr 4481  df-op 4485  df-uni 4752  df-br 4969  df-opab 5031  df-id 5355  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-iota 6196  df-fun 6234  df-fv 6240  df-ov 7026  df-oprab 7027  df-mpo 7028

This theorem is referenced by:  ovmpoga  7167  el2mpocsbcl  7643  suppval  7690  sprmpod  7748  mpocurryd  7793  erov  8251  cnfcomlem  9015  swrdval  13845  pfxval  13875  splval  13953  0csh0  13995  relexp0g  14219  relexpsucnnr  14222  relexp1g  14223  ramval  16177  prdsval  16561  prdsplusgval  16579  prdsmulrval  16581  prdsdsval  16584  prdsvscaval  16585  imasval  16617  imasdsval  16621  qusval  16648  homfval  16795  comffval  16802  comfval  16803  oppccofval  16819  ismon  16836  sectfval  16854  invfval  16862  cofuval  16985  cofu2nd  16988  resfval  16995  isnat  17050  fucval  17061  fucco  17065  setchom  17173  setcco  17176  catchom  17192  catcco  17194  estrchom  17210  estrcco  17213  funcestrcsetclem5  17227  funcsetcestrclem5  17242  xpcval  17260  xpcid  17272  1stf2  17276  2ndf2  17279  prfval  17282  prf2fval  17284  evlfval  17300  evlf2  17301  evlf2val  17302  evlf1  17303  curfval  17306  uncfval  17317  diagval  17323  hof2fval  17338  hof2val  17339  yonedalem4a  17358  gsumvalx  17713  mgm2nsgrplem2  17849  mgm2nsgrplem3  17850  sgrp2nmndlem2  17854  sgrp2nmndlem3  17855  pj1fval  18551  isrim0  19169  rmodislmodlem  19395  rmodislmod  19396  psrval  19834  selvffval  20016  frlmphl  20611  uvcfval  20614  mamufval  20682  mamuval  20683  mamufv  20684  matinvgcell  20732  mpomatmul  20743  mat1ov  20745  dmatval  20789  dmatmulcl  20797  scmatval  20801  scmatscmiddistr  20805  scmatscm  20810  mvmulfval  20839  mvmulval  20840  1mavmul  20845  maducoeval  20936  symgmatr01  20951  gsummatr01lem3  20954  gsummatr01lem4  20955  gsummatr01  20956  cpmat  21005  mat2pmatfval  21019  mat2pmatvalel  21021  mat2pmatmul  21027  cpm2mfval  21045  cpm2mvalel  21047  m2cpminvid  21049  m2cpminvid2  21051  decpmatval0  21060  decpmate  21062  decpmataa0  21064  decpmatmul  21068  pmatcollpw1  21072  monmatcollpw  21075  pmatcollpwlem  21076  pmatcollpw  21077  pmatcollpwscmatlem2  21086  pm2mpval  21091  pm2mpf1  21095  mptcoe1matfsupp  21098  mp2pm2mplem3  21104  mp2pm2mplem4  21105  chmatval  21125  chpmatfval  21126  chp0mat  21142  cnfval  21529  cnpfval  21530  fmval  22239  fmf  22241  fcfval  22329  tsmsval2  22425  blvalps  22682  blval  22683  ishtpy  23263  isphtpy  23272  rrxnm  23681  rrxmval  23695  rrxdsfival  23703  ehl2eudisval  23713  limcfval  24157  q1pval  24434  r1pval  24437  ismidb  26250  ttgitvval  26355  ebtwntg  26455  ecgrtg  26456  ewlksfval  27070  wwlksnon  27315  wspthsnon  27316  iswwlksnon  27317  iswspthsnon  27320  numclwlk1lem2  27837  ofoprabco  30095  fedgmul  30627  smatfval  30671  lmatfval  30690  mdetpmtr1  30699  ofcfval  30970  sitmfval  31221  sseqval  31259  sseqf  31263  sseqp1  31266  cndprobval  31304  orvcval  31328  reprval  31494  lpadval  31560  satf  32210  satefv  32271  mclsval  32420  fwddifnval  33235  finxpreclem1  34222  finxpreclem3  34226  ismtyval  34631  rrnmval  34659  rfovd  39853  fsovd  39860  fsovrfovd  39861  bccval  40229  fmuldfeqlem1  41426  rrndistlt  42139  hoidmvval  42423  hspval  42455  hoiqssbllem2  42469  smflimlem3  42613  copissgrp  43579  copisnmnd  43580  intopval  43609  rnghmval  43662  isrngisom  43667  rhmval  43690  cznrng  43726  rnghmsscmap2  43744  rnghmsscmap  43745  rngchomALTV  43756  rngccoALTV  43759  funcrngcsetc  43769  funcrngcsetcALT  43770  rhmsscmap2  43790  rhmsscmap  43791  funcringcsetc  43806  funcringcsetcALTV2lem5  43811  ringchomALTV  43819  ringccoALTV  43822  funcringcsetclem5ALTV  43834  srhmsubclem3  43846  srhmsubc  43847  fldhmsubc  43855  srhmsubcALTVlem2  43864  srhmsubcALTV  43865  fldhmsubcALTV  43873  lmod1lem1  44044  lmod1lem2  44045  lmod1lem3  44046  lmod1lem4  44047  lmod1lem5  44048  offval0  44067  fdivval  44102  digval  44161  rrx2plordisom  44213  sphere  44237