Theorem ovmpod 7552

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563   ∈ wcel 2145  (class class class)co 7400   ∈ cmpo 7402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-sbc 3748  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-opab 5168  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-iota 6481  df-fun 6527  df-fv 6533  df-ov 7403  df-oprab 7404  df-mpo 7405

This theorem is referenced by:  ovmpoga  7554  fvmpopr2d  7562  elovmpod  7644  el2mpocsbcl  8068  fsplitfpar  8101  suppval  8146  sprmpod  8208  mpocurryd  8253  erov  8800  cnfcomlem  9656  swrdval  14671  pfxval  14701  splval  14778  0csh0  14820  relexp0g  15049  relexpsucnnr  15052  relexp1g  15053  ramval  17058  prdsval  17498  prdsplusgval  17516  prdsmulrval  17518  prdsdsval  17521  prdsvscaval  17522  imasval  17555  imasdsval  17559  qusval  17586  homfval  17738  comffval  17745  comfval  17746  oppccofval  17762  ismon  17780  sectfval  17798  invfval  17806  cofuval  17929  cofu2nd  17932  resfval  17939  isnat  17997  fucval  18008  fucco  18012  setchom  18127  setcco  18130  catchom  18150  catcco  18152  estrchom  18173  estrcco  18176  funcestrcsetclem5  18190  funcsetcestrclem5  18205  xpcval  18223  xpcid  18235  1stf2  18239  2ndf2  18242  prfval  18245  prf2fval  18247  evlfval  18263  evlf2  18264  evlf2val  18265  evlf1  18266  curfval  18269  uncfval  18280  diagval  18286  hof2fval  18301  hof2val  18302  yonedalem4a  18321  gsumvalx  18724  mgm2nsgrplem2  18971  mgm2nsgrplem3  18972  sgrp2nmndlem2  18976  sgrp2nmndlem3  18977  pwmndgplus  18987  symgov  19445  pj1fval  19755  rnghmval  20513  isrngim  20518  isrim0  20555  rhmval  20573  rnghmsscmap2  20705  rnghmsscmap  20706  funcrngcsetc  20716  funcrngcsetcALT  20717  rhmsscmap2  20734  rhmsscmap  20735  funcringcsetc  20750  srhmsubclem3  20755  srhmsubc  20756  fldhmsubc  20857  rmodislmodlem  21019  rmodislmod  21020  frlmphl  21891  uvcfval  21894  psrval  22025  selvffval  22229  psdffval  22280  mamufval  22510  mamuval  22511  mamufv  22512  matinvgcell  22553  mpomatmul  22564  mat1ov  22566  dmatval  22610  dmatmulcl  22618  scmatval  22622  scmatscmiddistr  22626  scmatscm  22631  mvmulfval  22660  mvmulval  22661  1mavmul  22666  maducoeval  22757  symgmatr01  22772  gsummatr01lem3  22775  gsummatr01lem4  22776  gsummatr01  22777  cpmat  22827  mat2pmatfval  22841  mat2pmatvalel  22843  mat2pmatmul  22849  cpm2mfval  22867  cpm2mvalel  22869  m2cpminvid  22871  m2cpminvid2  22873  decpmatval0  22882  decpmate  22884  decpmataa0  22886  decpmatmul  22890  pmatcollpw1  22894  monmatcollpw  22897  pmatcollpwlem  22898  pmatcollpw  22899  pmatcollpwscmatlem2  22908  pm2mpval  22913  pm2mpf1  22917  mptcoe1matfsupp  22920  mp2pm2mplem3  22926  mp2pm2mplem4  22927  chmatval  22947  chpmatfval  22948  chp0mat  22964  cnfval  23351  cnpfval  23352  fmval  24061  fmf  24063  fcfval  24151  tsmsval2  24248  blvalps  24503  blval  24504  ishtpy  25092  isphtpy  25101  rrxnm  25511  rrxmval  25525  rrxdsfival  25533  ehl2eudisval  25543  limcfval  25992  q1pval  26273  r1pval  26276  ismidb  29030  ttgitvval  29140  ebtwntg  29241  ecgrtg  29242  ewlksfval  29860  wwlksnon  30109  wspthsnon  30110  iswwlksnon  30111  iswspthsnon  30114  numclwlk1lem2  30630  ofoprabco  32921  of0r  32936  mntoval  33215  mgcoval  33219  fxpval  33398  conjga  33403  cntrval2  33404  elrgspnlem2  33476  rlocaddval  33502  rlocmulval  33503  idlsrgmulrval  33716  extvval  33838  mplvrpmfgalem  33851  mplvrpmga  33852  mplvrpmmhm  33853  mplvrpmrhm  33854  splyval  33866  issply  33868  esplyval  33869  fedgmul  33938  smatfval  34102  lmatfval  34121  mdetpmtr1  34130  ofcfval  34405  sitmfval  34657  sseqval  34695  sseqf  34699  sseqp1  34702  cndprobval  34740  orvcval  34765  reprval  34914  lpadval  34983  satf  35716  satefv  35777  mclsval  35926  fwddifnval  36526  bj-imdirvallem  37684  finxpreclem1  37895  finxpreclem3  37899  ismtyval  38311  rrnmval  38339  isprimroot  42722  aks6d1c2p2  42748  aks6d1c2lem3  42755  aks6d1c2lem4  42756  aks6d1c6lem3  42801  ovmpogad  42865  tfsconcatun  43926  rfovd  44589  fsovd  44596  fsovrfovd  44597  mnringmulrvald  44815  bccval  44912  fmuldfeqlem1  46156  rrndistlt  46862  hoidmvval  47149  hspval  47181  hoiqssbllem2  47195  smflimlem3  47345  copissgrp  48788  copisnmnd  48789  intopval  48822  cznrng  48881  rngchomALTV  48888  rngccoALTV  48891  funcringcsetcALTV2lem5  48914  ringchomALTV  48922  ringccoALTV  48925  funcringcsetclem5ALTV  48937  srhmsubcALTVlem2  48944  srhmsubcALTV  48945  fldhmsubcALTV  48953  lmod1lem1  49118  lmod1lem2  49119  lmod1lem3  49120  lmod1lem4  49121  lmod1lem5  49122  fdivval  49170  digval  49229  itcoval1  49294  itcoval2  49295  itcoval3  49296  itcovalsucov  49299  ackvalsuc1mpt  49309  rrx2plordisom  49354  sphere  49378  iinfssclem3  49685  swapfval  49891  swapf2vala  49899  fucofvalg  49947  fuco112x  49961  fuco21  49965  fuco22  49968  prcofvalg  50005  prcof2a  50018  prcof2  50019  opf2fval  50034  functhinclem3  50075  incat  50230  lanfval  50242  ranfval  50243  lanval  50248  ranval  50249