Theorem ovmpod 7403

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108  (class class class)co 7255   ∈ cmpo 7257

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-iota 6376  df-fun 6420  df-fv 6426  df-ov 7258  df-oprab 7259  df-mpo 7260

This theorem is referenced by:  ovmpoga  7405  fvmpopr2d  7412  el2mpocsbcl  7896  fsplitfpar  7930  suppval  7950  sprmpod  8011  mpocurryd  8056  erov  8561  cnfcomlem  9387  swrdval  14284  pfxval  14314  splval  14392  0csh0  14434  relexp0g  14661  relexpsucnnr  14664  relexp1g  14665  ramval  16637  prdsval  17083  prdsplusgval  17101  prdsmulrval  17103  prdsdsval  17106  prdsvscaval  17107  imasval  17139  imasdsval  17143  qusval  17170  homfval  17318  comffval  17325  comfval  17326  oppccofval  17343  ismon  17362  sectfval  17380  invfval  17388  cofuval  17513  cofu2nd  17516  resfval  17523  isnat  17579  fucval  17591  fucco  17596  setchom  17711  setcco  17714  catchom  17734  catcco  17736  estrchom  17759  estrcco  17762  funcestrcsetclem5  17777  funcsetcestrclem5  17792  xpcval  17810  xpcid  17822  1stf2  17826  2ndf2  17829  prfval  17832  prf2fval  17834  evlfval  17851  evlf2  17852  evlf2val  17853  evlf1  17854  curfval  17857  uncfval  17868  diagval  17874  hof2fval  17889  hof2val  17890  yonedalem4a  17909  gsumvalx  18275  mgm2nsgrplem2  18473  mgm2nsgrplem3  18474  sgrp2nmndlem2  18478  sgrp2nmndlem3  18479  pwmndgplus  18489  symgov  18906  pj1fval  19215  isrim0  19882  rmodislmodlem  20105  rmodislmod  20106  rmodislmodOLD  20107  frlmphl  20898  uvcfval  20901  psrval  21028  selvffval  21236  mamufval  21444  mamuval  21445  mamufv  21446  matinvgcell  21492  mpomatmul  21503  mat1ov  21505  dmatval  21549  dmatmulcl  21557  scmatval  21561  scmatscmiddistr  21565  scmatscm  21570  mvmulfval  21599  mvmulval  21600  1mavmul  21605  maducoeval  21696  symgmatr01  21711  gsummatr01lem3  21714  gsummatr01lem4  21715  gsummatr01  21716  cpmat  21766  mat2pmatfval  21780  mat2pmatvalel  21782  mat2pmatmul  21788  cpm2mfval  21806  cpm2mvalel  21808  m2cpminvid  21810  m2cpminvid2  21812  decpmatval0  21821  decpmate  21823  decpmataa0  21825  decpmatmul  21829  pmatcollpw1  21833  monmatcollpw  21836  pmatcollpwlem  21837  pmatcollpw  21838  pmatcollpwscmatlem2  21847  pm2mpval  21852  pm2mpf1  21856  mptcoe1matfsupp  21859  mp2pm2mplem3  21865  mp2pm2mplem4  21866  chmatval  21886  chpmatfval  21887  chp0mat  21903  cnfval  22292  cnpfval  22293  fmval  23002  fmf  23004  fcfval  23092  tsmsval2  23189  blvalps  23446  blval  23447  ishtpy  24041  isphtpy  24050  rrxnm  24460  rrxmval  24474  rrxdsfival  24482  ehl2eudisval  24492  limcfval  24941  q1pval  25223  r1pval  25226  ismidb  27043  ttgitvval  27152  ebtwntg  27253  ecgrtg  27254  ewlksfval  27871  wwlksnon  28117  wspthsnon  28118  iswwlksnon  28119  iswspthsnon  28122  numclwlk1lem2  28635  ofoprabco  30903  mntoval  31162  mgcoval  31166  idlsrgmulrval  31556  fedgmul  31614  smatfval  31647  lmatfval  31666  mdetpmtr1  31675  ofcfval  31966  sitmfval  32217  sseqval  32255  sseqf  32259  sseqp1  32262  cndprobval  32300  orvcval  32324  reprval  32490  lpadval  32556  satf  33215  satefv  33276  mclsval  33425  fwddifnval  34392  bj-imdirvallem  35278  finxpreclem1  35487  finxpreclem3  35491  ismtyval  35885  rrnmval  35913  rfovd  41498  fsovd  41505  fsovrfovd  41506  mnringmulrvald  41734  bccval  41845  fmuldfeqlem1  43013  rrndistlt  43721  hoidmvval  44005  hspval  44037  hoiqssbllem2  44051  smflimlem3  44195  copissgrp  45250  copisnmnd  45251  intopval  45284  rnghmval  45337  isrngisom  45342  rhmval  45365  cznrng  45401  rnghmsscmap2  45419  rnghmsscmap  45420  rngchomALTV  45431  rngccoALTV  45434  funcrngcsetc  45444  funcrngcsetcALT  45445  rhmsscmap2  45465  rhmsscmap  45466  funcringcsetc  45481  funcringcsetcALTV2lem5  45486  ringchomALTV  45494  ringccoALTV  45497  funcringcsetclem5ALTV  45509  srhmsubclem3  45521  srhmsubc  45522  fldhmsubc  45530  srhmsubcALTVlem2  45539  srhmsubcALTV  45540  fldhmsubcALTV  45548  lmod1lem1  45716  lmod1lem2  45717  lmod1lem3  45718  lmod1lem4  45719  lmod1lem5  45720  fdivval  45773  digval  45832  itcoval1  45897  itcoval2  45898  itcoval3  45899  itcovalsucov  45902  ackvalsuc1mpt  45912  rrx2plordisom  45957  sphere  45981  functhinclem3  46212