Theorem ovmpod 7569

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  (class class class)co 7417   ∈ cmpo 7419

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-iota 6493  df-fun 6539  df-fv 6545  df-ov 7420  df-oprab 7421  df-mpo 7422

This theorem is used by:  ovmpoga  7571  fvmpopr2d  7579  elovmpod  7662  el2mpocsbcl  8086  fsplitfpar  8119  suppval  8164  sprmpod  8226  mpocurryd  8271  erov  8818  cnfcomlem  9682  swrdval  14715  pfxval  14747  splval  14824  0csh0  14868  relexp0g  15099  relexpsucnnr  15102  relexp1g  15103  ramval  17106  prdsval  17546  prdsplusgval  17564  prdsmulrval  17566  prdsdsval  17569  prdsvscaval  17570  imasval  17603  imasdsval  17607  qusval  17634  homfval  17786  comffval  17793  comfval  17794  oppccofval  17810  ismon  17828  sectfval  17846  invfval  17854  cofuval  17977  cofu2nd  17980  resfval  17987  isnat  18045  fucval  18056  fucco  18060  setchom  18175  setcco  18178  catchom  18198  catcco  18200  estrchom  18221  estrcco  18224  funcestrcsetclem5  18238  funcsetcestrclem5  18253  xpcval  18271  xpcid  18283  1stf2  18287  2ndf2  18290  prfval  18293  prf2fval  18295  evlfval  18311  evlf2  18312  evlf2val  18313  evlf1  18314  curfval  18317  uncfval  18328  diagval  18334  hof2fval  18349  hof2val  18350  yonedalem4a  18369  gsumvalx  18784  mgm2nsgrplem2  19037  mgm2nsgrplem3  19038  sgrp2nmndlem2  19042  sgrp2nmndlem3  19043  pwmndgplus  19060  symgov  19517  pj1fval  19827  rnghmval  20587  isrngim  20592  isrim0  20630  rhmval  20655  rnghmsscmap2  20797  rnghmsscmap  20798  funcrngcsetc  20808  funcrngcsetcALT  20809  rhmsscmap2  20826  rhmsscmap  20827  funcringcsetc  20842  srhmsubclem3  20847  srhmsubc  20848  fldhmsubc  20957  rmodislmodlem  21119  rmodislmod  21120  frlmphl  22000  uvcfval  22003  psrval  22136  selvffval  22340  psdffval  22391  mamufval  22620  mamuval  22621  mamufv  22622  matinvgcell  22663  mpomatmul  22674  mat1ov  22676  dmatval  22720  dmatmulcl  22728  scmatval  22732  scmatscmiddistr  22736  scmatscm  22741  mvmulfval  22770  mvmulval  22771  1mavmul  22776  maducoeval  22867  symgmatr01  22882  gsummatr01lem3  22885  gsummatr01lem4  22886  gsummatr01  22887  cpmat  22940  mat2pmatfval  22954  mat2pmatvalel  22956  mat2pmatmul  22962  cpm2mfval  22980  cpm2mvalel  22982  m2cpminvid  22984  m2cpminvid2  22986  decpmatval0  22995  decpmate  22997  decpmataa0  22999  decpmatmul  23003  pmatcollpw1  23007  monmatcollpw  23010  pmatcollpwlem  23011  pmatcollpw  23012  pmatcollpwscmatlem2  23021  pm2mpval  23026  pm2mpf1  23030  mptcoe1matfsupp  23033  mp2pm2mplem3  23039  mp2pm2mplem4  23040  chmatval  23060  chpmatfval  23061  chp0mat  23077  cnfval  23464  cnpfval  23465  fmval  24175  fmf  24177  fcfval  24265  tsmsval2  24362  blvalps  24617  blval  24618  ishtpy  25206  isphtpy  25215  rrxnm  25625  rrxmval  25639  rrxdsfival  25647  ehl2eudisval  25657  limcfval  26106  q1pval  26387  r1pval  26390  ismidb  29170  angmgmaddov1  29275  angmgmaddov2  29276  ttgitvval  29346  ebtwntg  29447  ecgrtg  29448  ewlksfval  30069  wwlksnon  30327  wspthsnon  30328  iswwlksnon  30329  iswspthsnon  30332  numclwlk1lem2  30858  ofoprabco  33145  of0r  33160  mntoval  33430  mgcoval  33434  fxpval  33613  conjga  33618  cntrval2  33619  elrgspnlem2  33691  rlocaddval  33717  rlocmulval  33718  idlsrgmulrval  33927  extvval  34049  mplvrpmfgalem  34062  mplvrpmga  34063  mplvrpmmhm  34064  mplvrpmrhm  34065  splyval  34077  issply  34079  esplyval  34080  fedgmul  34149  smatfval  34313  lmatfval  34332  mdetpmtr1  34341  ofcfval  34616  sitmfval  34869  sseqval  34907  sseqf  34911  sseqp1  34914  cndprobval  34952  orvcval  34977  reprval  35126  lpadval  35195  satf  35940  satefv  36001  mclsval  36150  fwddifnval  36751  bj-imdirvallem  37940  finxpreclem1  38151  finxpreclem3  38155  ismtyval  38558  rrnmval  38586  isprimroot  42967  aks6d1c2p2  42993  aks6d1c2lem3  43000  aks6d1c2lem4  43001  aks6d1c6lem3  43046  ovmpogad  43112  tfsconcatun  44186  rfovd  44849  fsovd  44856  fsovrfovd  44857  mnringmulrvald  45073  bccval  45170  fmuldfeqlem1  46420  rrndistlt  47126  hoidmvval  47413  hspval  47445  hoiqssbllem2  47459  smflimlem3  47609  copissgrp  49091  copisnmnd  49092  intopval  49125  cznrng  49184  rngchomALTV  49191  rngccoALTV  49194  funcringcsetcALTV2lem5  49217  ringchomALTV  49225  ringccoALTV  49228  funcringcsetclem5ALTV  49240  srhmsubcALTVlem2  49247  srhmsubcALTV  49248  fldhmsubcALTV  49256  lmod1lem1  49425  lmod1lem2  49426  lmod1lem3  49427  lmod1lem4  49428  lmod1lem5  49429  fdivval  49477  digval  49536  itcoval1  49601  itcoval2  49602  itcoval3  49603  itcovalsucov  49606  ackvalsuc1mpt  49616  rrx2plordisom  49661  sphere  49685  iinfssclem3  49990  swapfval  50196  swapf2vala  50204  fucofvalg  50252  fuco112x  50266  fuco21  50270  fuco22  50273  prcofvalg  50310  prcof2a  50323  prcof2  50324  opf2fval  50339  functhinclem3  50380  incat  50535  lanfval  50547  ranfval  50548  lanval  50553  ranval  50554  crosspdot0lem  50804