Theorem ovmpod 7466

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1540   ∈ wcel 2105  (class class class)co 7316   ∈ cmpo 7318

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5237  ax-nul 5244  ax-pr 5366

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3442  df-sbc 3726  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-nul 4267  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4850  df-br 5087  df-opab 5149  df-id 5506  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-iota 6417  df-fun 6467  df-fv 6473  df-ov 7319  df-oprab 7320  df-mpo 7321

This theorem is referenced by:  ovmpoga  7468  fvmpopr2d  7475  el2mpocsbcl  7971  fsplitfpar  8004  suppval  8027  sprmpod  8088  mpocurryd  8133  erov  8652  cnfcomlem  9534  swrdval  14432  pfxval  14462  splval  14540  0csh0  14582  relexp0g  14809  relexpsucnnr  14812  relexp1g  14813  ramval  16783  prdsval  17240  prdsplusgval  17258  prdsmulrval  17260  prdsdsval  17263  prdsvscaval  17264  imasval  17296  imasdsval  17300  qusval  17327  homfval  17475  comffval  17482  comfval  17483  oppccofval  17500  ismon  17519  sectfval  17537  invfval  17545  cofuval  17671  cofu2nd  17674  resfval  17681  isnat  17737  fucval  17749  fucco  17754  setchom  17869  setcco  17872  catchom  17892  catcco  17894  estrchom  17917  estrcco  17920  funcestrcsetclem5  17935  funcsetcestrclem5  17950  xpcval  17968  xpcid  17980  1stf2  17984  2ndf2  17987  prfval  17990  prf2fval  17992  evlfval  18009  evlf2  18010  evlf2val  18011  evlf1  18012  curfval  18015  uncfval  18026  diagval  18032  hof2fval  18047  hof2val  18048  yonedalem4a  18067  gsumvalx  18434  mgm2nsgrplem2  18631  mgm2nsgrplem3  18632  sgrp2nmndlem2  18636  sgrp2nmndlem3  18637  pwmndgplus  18647  symgov  19064  pj1fval  19372  isrim0  20039  rmodislmodlem  20270  rmodislmod  20271  rmodislmodOLD  20272  frlmphl  21068  uvcfval  21071  psrval  21198  selvffval  21406  mamufval  21614  mamuval  21615  mamufv  21616  matinvgcell  21664  mpomatmul  21675  mat1ov  21677  dmatval  21721  dmatmulcl  21729  scmatval  21733  scmatscmiddistr  21737  scmatscm  21742  mvmulfval  21771  mvmulval  21772  1mavmul  21777  maducoeval  21868  symgmatr01  21883  gsummatr01lem3  21886  gsummatr01lem4  21887  gsummatr01  21888  cpmat  21938  mat2pmatfval  21952  mat2pmatvalel  21954  mat2pmatmul  21960  cpm2mfval  21978  cpm2mvalel  21980  m2cpminvid  21982  m2cpminvid2  21984  decpmatval0  21993  decpmate  21995  decpmataa0  21997  decpmatmul  22001  pmatcollpw1  22005  monmatcollpw  22008  pmatcollpwlem  22009  pmatcollpw  22010  pmatcollpwscmatlem2  22019  pm2mpval  22024  pm2mpf1  22028  mptcoe1matfsupp  22031  mp2pm2mplem3  22037  mp2pm2mplem4  22038  chmatval  22058  chpmatfval  22059  chp0mat  22075  cnfval  22464  cnpfval  22465  fmval  23174  fmf  23176  fcfval  23264  tsmsval2  23361  blvalps  23618  blval  23619  ishtpy  24215  isphtpy  24224  rrxnm  24635  rrxmval  24649  rrxdsfival  24657  ehl2eudisval  24667  limcfval  25116  q1pval  25398  r1pval  25401  ismidb  27272  ttgitvval  27382  ebtwntg  27483  ecgrtg  27484  ewlksfval  28101  wwlksnon  28348  wspthsnon  28349  iswwlksnon  28350  iswspthsnon  28353  numclwlk1lem2  28866  ofoprabco  31132  mntoval  31391  mgcoval  31395  idlsrgmulrval  31789  fedgmul  31848  smatfval  31881  lmatfval  31900  mdetpmtr1  31909  ofcfval  32202  sitmfval  32453  sseqval  32491  sseqf  32495  sseqp1  32498  cndprobval  32536  orvcval  32560  reprval  32726  lpadval  32792  satf  33450  satefv  33511  mclsval  33660  fwddifnval  34535  bj-imdirvallem  35428  finxpreclem1  35637  finxpreclem3  35641  ismtyval  36035  rrnmval  36063  aks6d1c2p2  40326  rfovd  41848  fsovd  41855  fsovrfovd  41856  mnringmulrvald  42084  bccval  42195  fmuldfeqlem1  43378  rrndistlt  44086  hoidmvval  44371  hspval  44403  hoiqssbllem2  44417  smflimlem3  44567  copissgrp  45632  copisnmnd  45633  intopval  45666  rnghmval  45719  isrngisom  45724  rhmval  45747  cznrng  45783  rnghmsscmap2  45801  rnghmsscmap  45802  rngchomALTV  45813  rngccoALTV  45816  funcrngcsetc  45826  funcrngcsetcALT  45827  rhmsscmap2  45847  rhmsscmap  45848  funcringcsetc  45863  funcringcsetcALTV2lem5  45868  ringchomALTV  45876  ringccoALTV  45879  funcringcsetclem5ALTV  45891  srhmsubclem3  45903  srhmsubc  45904  fldhmsubc  45912  srhmsubcALTVlem2  45921  srhmsubcALTV  45922  fldhmsubcALTV  45930  lmod1lem1  46098  lmod1lem2  46099  lmod1lem3  46100  lmod1lem4  46101  lmod1lem5  46102  fdivval  46155  digval  46214  itcoval1  46279  itcoval2  46280  itcoval3  46281  itcovalsucov  46284  ackvalsuc1mpt  46294  rrx2plordisom  46339  sphere  46363  functhinclem3  46594