Theorem ovmpod 7302

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114  (class class class)co 7156   ∈ cmpo 7158

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-iota 6314  df-fun 6357  df-fv 6363  df-ov 7159  df-oprab 7160  df-mpo 7161

This theorem is referenced by:  ovmpoga  7304  el2mpocsbcl  7780  fsplitfpar  7814  suppval  7832  sprmpod  7890  mpocurryd  7935  erov  8394  cnfcomlem  9162  swrdval  14005  pfxval  14035  splval  14113  0csh0  14155  relexp0g  14381  relexpsucnnr  14384  relexp1g  14385  ramval  16344  prdsval  16728  prdsplusgval  16746  prdsmulrval  16748  prdsdsval  16751  prdsvscaval  16752  imasval  16784  imasdsval  16788  qusval  16815  homfval  16962  comffval  16969  comfval  16970  oppccofval  16986  ismon  17003  sectfval  17021  invfval  17029  cofuval  17152  cofu2nd  17155  resfval  17162  isnat  17217  fucval  17228  fucco  17232  setchom  17340  setcco  17343  catchom  17359  catcco  17361  estrchom  17377  estrcco  17380  funcestrcsetclem5  17394  funcsetcestrclem5  17409  xpcval  17427  xpcid  17439  1stf2  17443  2ndf2  17446  prfval  17449  prf2fval  17451  evlfval  17467  evlf2  17468  evlf2val  17469  evlf1  17470  curfval  17473  uncfval  17484  diagval  17490  hof2fval  17505  hof2val  17506  yonedalem4a  17525  gsumvalx  17886  mgm2nsgrplem2  18084  mgm2nsgrplem3  18085  sgrp2nmndlem2  18089  sgrp2nmndlem3  18090  pwmndgplus  18100  symgov  18512  pj1fval  18820  isrim0  19475  rmodislmodlem  19701  rmodislmod  19702  psrval  20142  selvffval  20329  frlmphl  20925  uvcfval  20928  mamufval  20996  mamuval  20997  mamufv  20998  matinvgcell  21044  mpomatmul  21055  mat1ov  21057  dmatval  21101  dmatmulcl  21109  scmatval  21113  scmatscmiddistr  21117  scmatscm  21122  mvmulfval  21151  mvmulval  21152  1mavmul  21157  maducoeval  21248  symgmatr01  21263  gsummatr01lem3  21266  gsummatr01lem4  21267  gsummatr01  21268  cpmat  21317  mat2pmatfval  21331  mat2pmatvalel  21333  mat2pmatmul  21339  cpm2mfval  21357  cpm2mvalel  21359  m2cpminvid  21361  m2cpminvid2  21363  decpmatval0  21372  decpmate  21374  decpmataa0  21376  decpmatmul  21380  pmatcollpw1  21384  monmatcollpw  21387  pmatcollpwlem  21388  pmatcollpw  21389  pmatcollpwscmatlem2  21398  pm2mpval  21403  pm2mpf1  21407  mptcoe1matfsupp  21410  mp2pm2mplem3  21416  mp2pm2mplem4  21417  chmatval  21437  chpmatfval  21438  chp0mat  21454  cnfval  21841  cnpfval  21842  fmval  22551  fmf  22553  fcfval  22641  tsmsval2  22738  blvalps  22995  blval  22996  ishtpy  23576  isphtpy  23585  rrxnm  23994  rrxmval  24008  rrxdsfival  24016  ehl2eudisval  24026  limcfval  24470  q1pval  24747  r1pval  24750  ismidb  26564  ttgitvval  26668  ebtwntg  26768  ecgrtg  26769  ewlksfval  27383  wwlksnon  27629  wspthsnon  27630  iswwlksnon  27631  iswspthsnon  27634  numclwlk1lem2  28149  ofoprabco  30409  fedgmul  31027  smatfval  31060  lmatfval  31079  mdetpmtr1  31088  ofcfval  31357  sitmfval  31608  sseqval  31646  sseqf  31650  sseqp1  31653  cndprobval  31691  orvcval  31715  reprval  31881  lpadval  31947  satf  32600  satefv  32661  mclsval  32810  fwddifnval  33624  bj-imdirval  34475  finxpreclem1  34673  finxpreclem3  34677  ismtyval  35093  rrnmval  35121  rfovd  40367  fsovd  40374  fsovrfovd  40375  bccval  40690  fmuldfeqlem1  41883  rrndistlt  42595  hoidmvval  42879  hspval  42911  hoiqssbllem2  42925  smflimlem3  43069  copissgrp  44095  copisnmnd  44096  intopval  44129  rnghmval  44182  isrngisom  44187  rhmval  44210  cznrng  44246  rnghmsscmap2  44264  rnghmsscmap  44265  rngchomALTV  44276  rngccoALTV  44279  funcrngcsetc  44289  funcrngcsetcALT  44290  rhmsscmap2  44310  rhmsscmap  44311  funcringcsetc  44326  funcringcsetcALTV2lem5  44331  ringchomALTV  44339  ringccoALTV  44342  funcringcsetclem5ALTV  44354  srhmsubclem3  44366  srhmsubc  44367  fldhmsubc  44375  srhmsubcALTVlem2  44384  srhmsubcALTV  44385  fldhmsubcALTV  44393  lmod1lem1  44562  lmod1lem2  44563  lmod1lem3  44564  lmod1lem4  44565  lmod1lem5  44566  fdivval  44619  digval  44678  rrx2plordisom  44730  sphere  44754