Theorem ovmpod 7519

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  (class class class)co 7367   ∈ cmpo 7369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-iota 6454  df-fun 6500  df-fv 6506  df-ov 7370  df-oprab 7371  df-mpo 7372

This theorem is referenced by:  ovmpoga  7521  fvmpopr2d  7529  elovmpod  7611  el2mpocsbcl  8035  fsplitfpar  8068  suppval  8112  sprmpod  8174  mpocurryd  8219  erov  8761  cnfcomlem  9620  swrdval  14606  pfxval  14636  splval  14713  0csh0  14755  relexp0g  14984  relexpsucnnr  14987  relexp1g  14988  ramval  16979  prdsval  17418  prdsplusgval  17436  prdsmulrval  17438  prdsdsval  17441  prdsvscaval  17442  imasval  17475  imasdsval  17479  qusval  17506  homfval  17658  comffval  17665  comfval  17666  oppccofval  17682  ismon  17700  sectfval  17718  invfval  17726  cofuval  17849  cofu2nd  17852  resfval  17859  isnat  17917  fucval  17928  fucco  17932  setchom  18047  setcco  18050  catchom  18070  catcco  18072  estrchom  18093  estrcco  18096  funcestrcsetclem5  18110  funcsetcestrclem5  18125  xpcval  18143  xpcid  18155  1stf2  18159  2ndf2  18162  prfval  18165  prf2fval  18167  evlfval  18183  evlf2  18184  evlf2val  18185  evlf1  18186  curfval  18189  uncfval  18200  diagval  18206  hof2fval  18221  hof2val  18222  yonedalem4a  18241  gsumvalx  18644  mgm2nsgrplem2  18890  mgm2nsgrplem3  18891  sgrp2nmndlem2  18895  sgrp2nmndlem3  18896  pwmndgplus  18906  symgov  19359  pj1fval  19669  rnghmval  20420  isrngim  20425  isrim0  20462  rhmval  20477  rnghmsscmap2  20606  rnghmsscmap  20607  funcrngcsetc  20617  funcrngcsetcALT  20618  rhmsscmap2  20635  rhmsscmap  20636  funcringcsetc  20651  srhmsubclem3  20656  srhmsubc  20657  fldhmsubc  20762  rmodislmodlem  20924  rmodislmod  20925  frlmphl  21761  uvcfval  21764  psrval  21895  selvffval  22099  psdffval  22123  mamufval  22357  mamuval  22358  mamufv  22359  matinvgcell  22400  mpomatmul  22411  mat1ov  22413  dmatval  22457  dmatmulcl  22465  scmatval  22469  scmatscmiddistr  22473  scmatscm  22478  mvmulfval  22507  mvmulval  22508  1mavmul  22513  maducoeval  22604  symgmatr01  22619  gsummatr01lem3  22622  gsummatr01lem4  22623  gsummatr01  22624  cpmat  22674  mat2pmatfval  22688  mat2pmatvalel  22690  mat2pmatmul  22696  cpm2mfval  22714  cpm2mvalel  22716  m2cpminvid  22718  m2cpminvid2  22720  decpmatval0  22729  decpmate  22731  decpmataa0  22733  decpmatmul  22737  pmatcollpw1  22741  monmatcollpw  22744  pmatcollpwlem  22745  pmatcollpw  22746  pmatcollpwscmatlem2  22755  pm2mpval  22760  pm2mpf1  22764  mptcoe1matfsupp  22767  mp2pm2mplem3  22773  mp2pm2mplem4  22774  chmatval  22794  chpmatfval  22795  chp0mat  22811  cnfval  23198  cnpfval  23199  fmval  23908  fmf  23910  fcfval  23998  tsmsval2  24095  blvalps  24350  blval  24351  ishtpy  24939  isphtpy  24948  rrxnm  25358  rrxmval  25372  rrxdsfival  25380  ehl2eudisval  25390  limcfval  25839  q1pval  26120  r1pval  26123  ismidb  28846  ttgitvval  28950  ebtwntg  29051  ecgrtg  29052  ewlksfval  29670  wwlksnon  29919  wspthsnon  29920  iswwlksnon  29921  iswspthsnon  29924  numclwlk1lem2  30440  ofoprabco  32737  of0r  32752  mntoval  33042  mgcoval  33046  fxpval  33226  conjga  33231  cntrval2  33232  elrgspnlem2  33304  rlocaddval  33329  rlocmulval  33330  idlsrgmulrval  33569  extvval  33675  mplvrpmfgalem  33688  mplvrpmga  33689  mplvrpmmhm  33690  mplvrpmrhm  33691  splyval  33703  issply  33705  esplyval  33706  fedgmul  33775  smatfval  33939  lmatfval  33958  mdetpmtr1  33967  ofcfval  34242  sitmfval  34494  sseqval  34532  sseqf  34536  sseqp1  34539  cndprobval  34577  orvcval  34602  reprval  34754  lpadval  34820  satf  35535  satefv  35596  mclsval  35745  fwddifnval  36345  bj-imdirvallem  37494  finxpreclem1  37705  finxpreclem3  37709  ismtyval  38121  rrnmval  38149  isprimroot  42532  aks6d1c2p2  42558  aks6d1c2lem3  42565  aks6d1c2lem4  42566  aks6d1c6lem3  42611  ovmpogad  42676  tfsconcatun  43765  rfovd  44428  fsovd  44435  fsovrfovd  44436  mnringmulrvald  44654  bccval  44765  fmuldfeqlem1  46012  rrndistlt  46718  hoidmvval  47005  hspval  47037  hoiqssbllem2  47051  smflimlem3  47201  copissgrp  48644  copisnmnd  48645  intopval  48678  cznrng  48737  rngchomALTV  48744  rngccoALTV  48747  funcringcsetcALTV2lem5  48770  ringchomALTV  48778  ringccoALTV  48781  funcringcsetclem5ALTV  48793  srhmsubcALTVlem2  48800  srhmsubcALTV  48801  fldhmsubcALTV  48809  lmod1lem1  48963  lmod1lem2  48964  lmod1lem3  48965  lmod1lem4  48966  lmod1lem5  48967  fdivval  49015  digval  49074  itcoval1  49139  itcoval2  49140  itcoval3  49141  itcovalsucov  49144  ackvalsuc1mpt  49154  rrx2plordisom  49199  sphere  49223  iinfssclem3  49531  swapfval  49737  swapf2vala  49745  fucofvalg  49793  fuco112x  49807  fuco21  49811  fuco22  49814  prcofvalg  49851  prcof2a  49864  prcof2  49865  opf2fval  49880  functhinclem3  49921  incat  50076  lanfval  50088  ranfval  50089  lanval  50094  ranval  50095