Theorem ovmpod 7585

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 7584	1 ⊢ (𝜑 → (𝐴𝐹𝐵) = 𝑆)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  (class class class)co 7431   ∈ cmpo 7433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-iota 6514  df-fun 6563  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436

This theorem is referenced by:  ovmpoga  7587  fvmpopr2d  7595  elovmpod  7677  el2mpocsbcl  8110  fsplitfpar  8143  suppval  8187  sprmpod  8249  mpocurryd  8294  erov  8854  cnfcomlem  9739  swrdval  14681  pfxval  14711  splval  14789  0csh0  14831  relexp0g  15061  relexpsucnnr  15064  relexp1g  15065  ramval  17046  prdsval  17500  prdsplusgval  17518  prdsmulrval  17520  prdsdsval  17523  prdsvscaval  17524  imasval  17556  imasdsval  17560  qusval  17587  homfval  17735  comffval  17742  comfval  17743  oppccofval  17759  ismon  17777  sectfval  17795  invfval  17803  cofuval  17927  cofu2nd  17930  resfval  17937  isnat  17995  fucval  18006  fucco  18010  setchom  18125  setcco  18128  catchom  18148  catcco  18150  estrchom  18171  estrcco  18174  funcestrcsetclem5  18189  funcsetcestrclem5  18204  xpcval  18222  xpcid  18234  1stf2  18238  2ndf2  18241  prfval  18244  prf2fval  18246  evlfval  18262  evlf2  18263  evlf2val  18264  evlf1  18265  curfval  18268  uncfval  18279  diagval  18285  hof2fval  18300  hof2val  18301  yonedalem4a  18320  gsumvalx  18689  mgm2nsgrplem2  18932  mgm2nsgrplem3  18933  sgrp2nmndlem2  18937  sgrp2nmndlem3  18938  pwmndgplus  18948  symgov  19401  pj1fval  19712  rnghmval  20440  isrngim  20445  isrim0OLD  20481  isrim0  20483  rhmval  20500  rnghmsscmap2  20629  rnghmsscmap  20630  funcrngcsetc  20640  funcrngcsetcALT  20641  rhmsscmap2  20658  rhmsscmap  20659  funcringcsetc  20674  srhmsubclem3  20679  srhmsubc  20680  fldhmsubc  20786  rmodislmodlem  20927  rmodislmod  20928  frlmphl  21801  uvcfval  21804  psrval  21935  selvffval  22137  psdffval  22161  mamufval  22396  mamuval  22397  mamufv  22398  matinvgcell  22441  mpomatmul  22452  mat1ov  22454  dmatval  22498  dmatmulcl  22506  scmatval  22510  scmatscmiddistr  22514  scmatscm  22519  mvmulfval  22548  mvmulval  22549  1mavmul  22554  maducoeval  22645  symgmatr01  22660  gsummatr01lem3  22663  gsummatr01lem4  22664  gsummatr01  22665  cpmat  22715  mat2pmatfval  22729  mat2pmatvalel  22731  mat2pmatmul  22737  cpm2mfval  22755  cpm2mvalel  22757  m2cpminvid  22759  m2cpminvid2  22761  decpmatval0  22770  decpmate  22772  decpmataa0  22774  decpmatmul  22778  pmatcollpw1  22782  monmatcollpw  22785  pmatcollpwlem  22786  pmatcollpw  22787  pmatcollpwscmatlem2  22796  pm2mpval  22801  pm2mpf1  22805  mptcoe1matfsupp  22808  mp2pm2mplem3  22814  mp2pm2mplem4  22815  chmatval  22835  chpmatfval  22836  chp0mat  22852  cnfval  23241  cnpfval  23242  fmval  23951  fmf  23953  fcfval  24041  tsmsval2  24138  blvalps  24395  blval  24396  ishtpy  25004  isphtpy  25013  rrxnm  25425  rrxmval  25439  rrxdsfival  25447  ehl2eudisval  25457  limcfval  25907  q1pval  26194  r1pval  26197  ismidb  28786  ttgitvval  28896  ebtwntg  28997  ecgrtg  28998  ewlksfval  29619  wwlksnon  29871  wspthsnon  29872  iswwlksnon  29873  iswspthsnon  29876  numclwlk1lem2  30389  ofoprabco  32674  of0r  32688  mntoval  32972  mgcoval  32976  elrgspnlem2  33247  rlocaddval  33272  rlocmulval  33273  idlsrgmulrval  33537  fedgmul  33682  smatfval  33794  lmatfval  33813  mdetpmtr1  33822  ofcfval  34099  sitmfval  34352  sseqval  34390  sseqf  34394  sseqp1  34397  cndprobval  34435  orvcval  34460  reprval  34625  lpadval  34691  satf  35358  satefv  35419  mclsval  35568  fwddifnval  36164  bj-imdirvallem  37181  finxpreclem1  37390  finxpreclem3  37394  ismtyval  37807  rrnmval  37835  isprimroot  42094  aks6d1c2p2  42120  aks6d1c2lem3  42127  aks6d1c2lem4  42128  aks6d1c6lem3  42173  ovmpogad  42276  tfsconcatun  43350  rfovd  44014  fsovd  44021  fsovrfovd  44022  mnringmulrvald  44246  bccval  44357  fmuldfeqlem1  45597  rrndistlt  46305  hoidmvval  46592  hspval  46624  hoiqssbllem2  46638  smflimlem3  46788  copissgrp  48084  copisnmnd  48085  intopval  48118  cznrng  48177  rngchomALTV  48184  rngccoALTV  48187  funcringcsetcALTV2lem5  48210  ringchomALTV  48218  ringccoALTV  48221  funcringcsetclem5ALTV  48233  srhmsubcALTVlem2  48240  srhmsubcALTV  48241  fldhmsubcALTV  48249  lmod1lem1  48404  lmod1lem2  48405  lmod1lem3  48406  lmod1lem4  48407  lmod1lem5  48408  fdivval  48460  digval  48519  itcoval1  48584  itcoval2  48585  itcoval3  48586  itcovalsucov  48589  ackvalsuc1mpt  48599  rrx2plordisom  48644  sphere  48668  swapfval  48968  swapf2vala  48976  fucofvalg  49013  fuco112x  49027  fuco21  49031  fuco22  49034  functhinclem3  49095