Theorem ovmpod 7434

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2107  (class class class)co 7284   ∈ cmpo 7286

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 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-sbc 3718  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-iota 6395  df-fun 6439  df-fv 6445  df-ov 7287  df-oprab 7288  df-mpo 7289

This theorem is referenced by:  ovmpoga  7436  fvmpopr2d  7443  el2mpocsbcl  7934  fsplitfpar  7968  suppval  7988  sprmpod  8049  mpocurryd  8094  erov  8612  cnfcomlem  9466  swrdval  14365  pfxval  14395  splval  14473  0csh0  14515  relexp0g  14742  relexpsucnnr  14745  relexp1g  14746  ramval  16718  prdsval  17175  prdsplusgval  17193  prdsmulrval  17195  prdsdsval  17198  prdsvscaval  17199  imasval  17231  imasdsval  17235  qusval  17262  homfval  17410  comffval  17417  comfval  17418  oppccofval  17435  ismon  17454  sectfval  17472  invfval  17480  cofuval  17606  cofu2nd  17609  resfval  17616  isnat  17672  fucval  17684  fucco  17689  setchom  17804  setcco  17807  catchom  17827  catcco  17829  estrchom  17852  estrcco  17855  funcestrcsetclem5  17870  funcsetcestrclem5  17885  xpcval  17903  xpcid  17915  1stf2  17919  2ndf2  17922  prfval  17925  prf2fval  17927  evlfval  17944  evlf2  17945  evlf2val  17946  evlf1  17947  curfval  17950  uncfval  17961  diagval  17967  hof2fval  17982  hof2val  17983  yonedalem4a  18002  gsumvalx  18369  mgm2nsgrplem2  18567  mgm2nsgrplem3  18568  sgrp2nmndlem2  18572  sgrp2nmndlem3  18573  pwmndgplus  18583  symgov  19000  pj1fval  19309  isrim0  19976  rmodislmodlem  20199  rmodislmod  20200  rmodislmodOLD  20201  frlmphl  20997  uvcfval  21000  psrval  21127  selvffval  21335  mamufval  21543  mamuval  21544  mamufv  21545  matinvgcell  21593  mpomatmul  21604  mat1ov  21606  dmatval  21650  dmatmulcl  21658  scmatval  21662  scmatscmiddistr  21666  scmatscm  21671  mvmulfval  21700  mvmulval  21701  1mavmul  21706  maducoeval  21797  symgmatr01  21812  gsummatr01lem3  21815  gsummatr01lem4  21816  gsummatr01  21817  cpmat  21867  mat2pmatfval  21881  mat2pmatvalel  21883  mat2pmatmul  21889  cpm2mfval  21907  cpm2mvalel  21909  m2cpminvid  21911  m2cpminvid2  21913  decpmatval0  21922  decpmate  21924  decpmataa0  21926  decpmatmul  21930  pmatcollpw1  21934  monmatcollpw  21937  pmatcollpwlem  21938  pmatcollpw  21939  pmatcollpwscmatlem2  21948  pm2mpval  21953  pm2mpf1  21957  mptcoe1matfsupp  21960  mp2pm2mplem3  21966  mp2pm2mplem4  21967  chmatval  21987  chpmatfval  21988  chp0mat  22004  cnfval  22393  cnpfval  22394  fmval  23103  fmf  23105  fcfval  23193  tsmsval2  23290  blvalps  23547  blval  23548  ishtpy  24144  isphtpy  24153  rrxnm  24564  rrxmval  24578  rrxdsfival  24586  ehl2eudisval  24596  limcfval  25045  q1pval  25327  r1pval  25330  ismidb  27148  ttgitvval  27258  ebtwntg  27359  ecgrtg  27360  ewlksfval  27977  wwlksnon  28225  wspthsnon  28226  iswwlksnon  28227  iswspthsnon  28230  numclwlk1lem2  28743  ofoprabco  31010  mntoval  31269  mgcoval  31273  idlsrgmulrval  31663  fedgmul  31721  smatfval  31754  lmatfval  31773  mdetpmtr1  31782  ofcfval  32075  sitmfval  32326  sseqval  32364  sseqf  32368  sseqp1  32371  cndprobval  32409  orvcval  32433  reprval  32599  lpadval  32665  satf  33324  satefv  33385  mclsval  33534  fwddifnval  34474  bj-imdirvallem  35360  finxpreclem1  35569  finxpreclem3  35573  ismtyval  35967  rrnmval  35995  rfovd  41616  fsovd  41623  fsovrfovd  41624  mnringmulrvald  41852  bccval  41963  fmuldfeqlem1  43130  rrndistlt  43838  hoidmvval  44122  hspval  44154  hoiqssbllem2  44168  smflimlem3  44318  copissgrp  45373  copisnmnd  45374  intopval  45407  rnghmval  45460  isrngisom  45465  rhmval  45488  cznrng  45524  rnghmsscmap2  45542  rnghmsscmap  45543  rngchomALTV  45554  rngccoALTV  45557  funcrngcsetc  45567  funcrngcsetcALT  45568  rhmsscmap2  45588  rhmsscmap  45589  funcringcsetc  45604  funcringcsetcALTV2lem5  45609  ringchomALTV  45617  ringccoALTV  45620  funcringcsetclem5ALTV  45632  srhmsubclem3  45644  srhmsubc  45645  fldhmsubc  45653  srhmsubcALTVlem2  45662  srhmsubcALTV  45663  fldhmsubcALTV  45671  lmod1lem1  45839  lmod1lem2  45840  lmod1lem3  45841  lmod1lem4  45842  lmod1lem5  45843  fdivval  45896  digval  45955  itcoval1  46020  itcoval2  46021  itcoval3  46022  itcovalsucov  46025  ackvalsuc1mpt  46035  rrx2plordisom  46080  sphere  46104  functhinclem3  46335