Theorem ovmpod 7560

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  (class class class)co 7409   ∈ cmpo 7411

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-iota 6496  df-fun 6546  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414

This theorem is referenced by:  ovmpoga  7562  fvmpopr2d  7569  el2mpocsbcl  8071  fsplitfpar  8104  suppval  8148  sprmpod  8209  mpocurryd  8254  erov  8808  cnfcomlem  9694  swrdval  14593  pfxval  14623  splval  14701  0csh0  14743  relexp0g  14969  relexpsucnnr  14972  relexp1g  14973  ramval  16941  prdsval  17401  prdsplusgval  17419  prdsmulrval  17421  prdsdsval  17424  prdsvscaval  17425  imasval  17457  imasdsval  17461  qusval  17488  homfval  17636  comffval  17643  comfval  17644  oppccofval  17661  ismon  17680  sectfval  17698  invfval  17706  cofuval  17832  cofu2nd  17835  resfval  17842  isnat  17898  fucval  17910  fucco  17915  setchom  18030  setcco  18033  catchom  18053  catcco  18055  estrchom  18078  estrcco  18081  funcestrcsetclem5  18096  funcsetcestrclem5  18111  xpcval  18129  xpcid  18141  1stf2  18145  2ndf2  18148  prfval  18151  prf2fval  18153  evlfval  18170  evlf2  18171  evlf2val  18172  evlf1  18173  curfval  18176  uncfval  18187  diagval  18193  hof2fval  18208  hof2val  18209  yonedalem4a  18228  gsumvalx  18595  mgm2nsgrplem2  18800  mgm2nsgrplem3  18801  sgrp2nmndlem2  18805  sgrp2nmndlem3  18806  pwmndgplus  18816  symgov  19251  pj1fval  19562  isrim0OLD  20259  isrim0  20261  rmodislmodlem  20539  rmodislmod  20540  rmodislmodOLD  20541  frlmphl  21336  uvcfval  21339  psrval  21468  selvffval  21679  mamufval  21887  mamuval  21888  mamufv  21889  matinvgcell  21937  mpomatmul  21948  mat1ov  21950  dmatval  21994  dmatmulcl  22002  scmatval  22006  scmatscmiddistr  22010  scmatscm  22015  mvmulfval  22044  mvmulval  22045  1mavmul  22050  maducoeval  22141  symgmatr01  22156  gsummatr01lem3  22159  gsummatr01lem4  22160  gsummatr01  22161  cpmat  22211  mat2pmatfval  22225  mat2pmatvalel  22227  mat2pmatmul  22233  cpm2mfval  22251  cpm2mvalel  22253  m2cpminvid  22255  m2cpminvid2  22257  decpmatval0  22266  decpmate  22268  decpmataa0  22270  decpmatmul  22274  pmatcollpw1  22278  monmatcollpw  22281  pmatcollpwlem  22282  pmatcollpw  22283  pmatcollpwscmatlem2  22292  pm2mpval  22297  pm2mpf1  22301  mptcoe1matfsupp  22304  mp2pm2mplem3  22310  mp2pm2mplem4  22311  chmatval  22331  chpmatfval  22332  chp0mat  22348  cnfval  22737  cnpfval  22738  fmval  23447  fmf  23449  fcfval  23537  tsmsval2  23634  blvalps  23891  blval  23892  ishtpy  24488  isphtpy  24497  rrxnm  24908  rrxmval  24922  rrxdsfival  24930  ehl2eudisval  24940  limcfval  25389  q1pval  25671  r1pval  25674  ismidb  28060  ttgitvval  28170  ebtwntg  28271  ecgrtg  28272  ewlksfval  28889  wwlksnon  29136  wspthsnon  29137  iswwlksnon  29138  iswspthsnon  29141  numclwlk1lem2  29654  ofoprabco  31920  mntoval  32183  mgcoval  32187  idlsrgmulrval  32654  fedgmul  32747  smatfval  32806  lmatfval  32825  mdetpmtr1  32834  ofcfval  33127  sitmfval  33380  sseqval  33418  sseqf  33422  sseqp1  33425  cndprobval  33463  orvcval  33487  reprval  33653  lpadval  33719  satf  34375  satefv  34436  mclsval  34585  fwddifnval  35166  bj-imdirvallem  36109  finxpreclem1  36318  finxpreclem3  36322  ismtyval  36716  rrnmval  36744  aks6d1c2p2  41005  ovmpogad  41105  tfsconcatun  42135  rfovd  42800  fsovd  42807  fsovrfovd  42808  mnringmulrvald  43034  bccval  43145  fmuldfeqlem1  44346  rrndistlt  45054  hoidmvval  45341  hspval  45373  hoiqssbllem2  45387  smflimlem3  45537  copissgrp  46626  copisnmnd  46627  intopval  46660  rnghmval  46737  isrngisom  46742  rhmval  46770  cznrng  46901  rnghmsscmap2  46919  rnghmsscmap  46920  rngchomALTV  46931  rngccoALTV  46934  funcrngcsetc  46944  funcrngcsetcALT  46945  rhmsscmap2  46965  rhmsscmap  46966  funcringcsetc  46981  funcringcsetcALTV2lem5  46986  ringchomALTV  46994  ringccoALTV  46997  funcringcsetclem5ALTV  47009  srhmsubclem3  47021  srhmsubc  47022  fldhmsubc  47030  srhmsubcALTVlem2  47039  srhmsubcALTV  47040  fldhmsubcALTV  47048  lmod1lem1  47216  lmod1lem2  47217  lmod1lem3  47218  lmod1lem4  47219  lmod1lem5  47220  fdivval  47273  digval  47332  itcoval1  47397  itcoval2  47398  itcoval3  47399  itcovalsucov  47402  ackvalsuc1mpt  47412  rrx2plordisom  47457  sphere  47481  functhinclem3  47711