Theorem ovmpod 7544

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559   ∈ wcel 2141  (class class class)co 7392   ∈ cmpo 7394

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3745  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-iota 6473  df-fun 6519  df-fv 6525  df-ov 7395  df-oprab 7396  df-mpo 7397

This theorem is referenced by:  ovmpoga  7546  fvmpopr2d  7554  elovmpod  7636  el2mpocsbcl  8059  fsplitfpar  8092  suppval  8137  sprmpod  8199  mpocurryd  8244  erov  8791  cnfcomlem  9651  swrdval  14654  pfxval  14684  splval  14761  0csh0  14803  relexp0g  15032  relexpsucnnr  15035  relexp1g  15036  ramval  17027  prdsval  17467  prdsplusgval  17485  prdsmulrval  17487  prdsdsval  17490  prdsvscaval  17491  imasval  17524  imasdsval  17528  qusval  17555  homfval  17707  comffval  17714  comfval  17715  oppccofval  17731  ismon  17749  sectfval  17767  invfval  17775  cofuval  17898  cofu2nd  17901  resfval  17908  isnat  17966  fucval  17977  fucco  17981  setchom  18096  setcco  18099  catchom  18119  catcco  18121  estrchom  18142  estrcco  18145  funcestrcsetclem5  18159  funcsetcestrclem5  18174  xpcval  18192  xpcid  18204  1stf2  18208  2ndf2  18211  prfval  18214  prf2fval  18216  evlfval  18232  evlf2  18233  evlf2val  18234  evlf1  18235  curfval  18238  uncfval  18249  diagval  18255  hof2fval  18270  hof2val  18271  yonedalem4a  18290  gsumvalx  18693  mgm2nsgrplem2  18939  mgm2nsgrplem3  18940  sgrp2nmndlem2  18944  sgrp2nmndlem3  18945  pwmndgplus  18955  symgov  19407  pj1fval  19717  rnghmval  20468  isrngim  20473  isrim0  20510  rhmval  20528  rnghmsscmap2  20658  rnghmsscmap  20659  funcrngcsetc  20669  funcrngcsetcALT  20670  rhmsscmap2  20687  rhmsscmap  20688  funcringcsetc  20703  srhmsubclem3  20708  srhmsubc  20709  fldhmsubc  20814  rmodislmodlem  20976  rmodislmod  20977  frlmphl  21813  uvcfval  21816  psrval  21947  selvffval  22151  psdffval  22202  mamufval  22432  mamuval  22433  mamufv  22434  matinvgcell  22475  mpomatmul  22486  mat1ov  22488  dmatval  22532  dmatmulcl  22540  scmatval  22544  scmatscmiddistr  22548  scmatscm  22553  mvmulfval  22582  mvmulval  22583  1mavmul  22588  maducoeval  22679  symgmatr01  22694  gsummatr01lem3  22697  gsummatr01lem4  22698  gsummatr01  22699  cpmat  22749  mat2pmatfval  22763  mat2pmatvalel  22765  mat2pmatmul  22771  cpm2mfval  22789  cpm2mvalel  22791  m2cpminvid  22793  m2cpminvid2  22795  decpmatval0  22804  decpmate  22806  decpmataa0  22808  decpmatmul  22812  pmatcollpw1  22816  monmatcollpw  22819  pmatcollpwlem  22820  pmatcollpw  22821  pmatcollpwscmatlem2  22830  pm2mpval  22835  pm2mpf1  22839  mptcoe1matfsupp  22842  mp2pm2mplem3  22848  mp2pm2mplem4  22849  chmatval  22869  chpmatfval  22870  chp0mat  22886  cnfval  23273  cnpfval  23274  fmval  23983  fmf  23985  fcfval  24073  tsmsval2  24170  blvalps  24425  blval  24426  ishtpy  25014  isphtpy  25023  rrxnm  25433  rrxmval  25447  rrxdsfival  25455  ehl2eudisval  25465  limcfval  25914  q1pval  26195  r1pval  26198  ismidb  28924  ttgitvval  29028  ebtwntg  29129  ecgrtg  29130  ewlksfval  29748  wwlksnon  29997  wspthsnon  29998  iswwlksnon  29999  iswspthsnon  30002  numclwlk1lem2  30518  ofoprabco  32816  of0r  32831  mntoval  33121  mgcoval  33125  fxpval  33306  conjga  33311  cntrval2  33312  elrgspnlem2  33385  rlocaddval  33411  rlocmulval  33412  idlsrgmulrval  33666  extvval  33789  mplvrpmfgalem  33802  mplvrpmga  33803  mplvrpmmhm  33804  mplvrpmrhm  33805  splyval  33817  issply  33819  esplyval  33820  fedgmul  33889  smatfval  34053  lmatfval  34072  mdetpmtr1  34081  ofcfval  34356  sitmfval  34608  sseqval  34646  sseqf  34650  sseqp1  34653  cndprobval  34691  orvcval  34716  reprval  34868  lpadval  34937  satf  35667  satefv  35728  mclsval  35877  fwddifnval  36477  bj-imdirvallem  37636  finxpreclem1  37847  finxpreclem3  37851  ismtyval  38263  rrnmval  38291  isprimroot  42674  aks6d1c2p2  42700  aks6d1c2lem3  42707  aks6d1c2lem4  42708  aks6d1c6lem3  42753  ovmpogad  42817  tfsconcatun  43878  rfovd  44541  fsovd  44548  fsovrfovd  44549  mnringmulrvald  44767  bccval  44878  fmuldfeqlem1  46122  rrndistlt  46828  hoidmvval  47115  hspval  47147  hoiqssbllem2  47161  smflimlem3  47311  copissgrp  48754  copisnmnd  48755  intopval  48788  cznrng  48847  rngchomALTV  48854  rngccoALTV  48857  funcringcsetcALTV2lem5  48880  ringchomALTV  48888  ringccoALTV  48891  funcringcsetclem5ALTV  48903  srhmsubcALTVlem2  48910  srhmsubcALTV  48911  fldhmsubcALTV  48919  lmod1lem1  49073  lmod1lem2  49074  lmod1lem3  49075  lmod1lem4  49076  lmod1lem5  49077  fdivval  49125  digval  49184  itcoval1  49249  itcoval2  49250  itcoval3  49251  itcovalsucov  49254  ackvalsuc1mpt  49264  rrx2plordisom  49309  sphere  49333  iinfssclem3  49641  swapfval  49847  swapf2vala  49855  fucofvalg  49903  fuco112x  49917  fuco21  49921  fuco22  49924  prcofvalg  49961  prcof2a  49974  prcof2  49975  opf2fval  49990  functhinclem3  50031  incat  50186  lanfval  50198  ranfval  50199  lanval  50204  ranval  50205