Theorem ovmpod 7575

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  (class class class)co 7423   ∈ cmpo 7425

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-pr 5409

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 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-sbc 3748  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-iota 6499  df-fun 6545  df-fv 6551  df-ov 7426  df-oprab 7427  df-mpo 7428

This theorem is used by:  ovmpoga  7577  fvmpopr2d  7585  elovmpod  7667  el2mpocsbcl  8089  fsplitfpar  8122  suppval  8167  sprmpod  8229  mpocurryd  8274  erov  8821  cnfcomlem  9678  swrdval  14703  pfxval  14735  splval  14812  0csh0  14856  relexp0g  15085  relexpsucnnr  15088  relexp1g  15089  ramval  17093  prdsval  17533  prdsplusgval  17551  prdsmulrval  17553  prdsdsval  17556  prdsvscaval  17557  imasval  17590  imasdsval  17594  qusval  17621  homfval  17773  comffval  17780  comfval  17781  oppccofval  17797  ismon  17815  sectfval  17833  invfval  17841  cofuval  17964  cofu2nd  17967  resfval  17974  isnat  18032  fucval  18043  fucco  18047  setchom  18162  setcco  18165  catchom  18185  catcco  18187  estrchom  18208  estrcco  18211  funcestrcsetclem5  18225  funcsetcestrclem5  18240  xpcval  18258  xpcid  18270  1stf2  18274  2ndf2  18277  prfval  18280  prf2fval  18282  evlfval  18298  evlf2  18299  evlf2val  18300  evlf1  18301  curfval  18304  uncfval  18315  diagval  18321  hof2fval  18336  hof2val  18337  yonedalem4a  18356  gsumvalx  18763  mgm2nsgrplem2  19012  mgm2nsgrplem3  19013  sgrp2nmndlem2  19017  sgrp2nmndlem3  19018  pwmndgplus  19028  symgov  19485  pj1fval  19795  rnghmval  20555  isrngim  20560  isrim0  20598  rhmval  20623  rnghmsscmap2  20765  rnghmsscmap  20766  funcrngcsetc  20776  funcrngcsetcALT  20777  rhmsscmap2  20794  rhmsscmap  20795  funcringcsetc  20810  srhmsubclem3  20815  srhmsubc  20816  fldhmsubc  20925  rmodislmodlem  21087  rmodislmod  21088  frlmphl  21968  uvcfval  21971  psrval  22102  selvffval  22306  psdffval  22357  mamufval  22586  mamuval  22587  mamufv  22588  matinvgcell  22629  mpomatmul  22640  mat1ov  22642  dmatval  22686  dmatmulcl  22694  scmatval  22698  scmatscmiddistr  22702  scmatscm  22707  mvmulfval  22736  mvmulval  22737  1mavmul  22742  maducoeval  22833  symgmatr01  22848  gsummatr01lem3  22851  gsummatr01lem4  22852  gsummatr01  22853  cpmat  22903  mat2pmatfval  22917  mat2pmatvalel  22919  mat2pmatmul  22925  cpm2mfval  22943  cpm2mvalel  22945  m2cpminvid  22947  m2cpminvid2  22949  decpmatval0  22958  decpmate  22960  decpmataa0  22962  decpmatmul  22966  pmatcollpw1  22970  monmatcollpw  22973  pmatcollpwlem  22974  pmatcollpw  22975  pmatcollpwscmatlem2  22984  pm2mpval  22989  pm2mpf1  22993  mptcoe1matfsupp  22996  mp2pm2mplem3  23002  mp2pm2mplem4  23003  chmatval  23023  chpmatfval  23024  chp0mat  23040  cnfval  23427  cnpfval  23428  fmval  24137  fmf  24139  fcfval  24227  tsmsval2  24324  blvalps  24579  blval  24580  ishtpy  25168  isphtpy  25177  rrxnm  25587  rrxmval  25601  rrxdsfival  25609  ehl2eudisval  25619  limcfval  26068  q1pval  26349  r1pval  26352  ismidb  29124  ttgitvval  29268  ebtwntg  29369  ecgrtg  29370  ewlksfval  29988  wwlksnon  30237  wspthsnon  30238  iswwlksnon  30239  iswspthsnon  30242  numclwlk1lem2  30758  ofoprabco  33046  of0r  33061  mntoval  33333  mgcoval  33337  fxpval  33516  conjga  33521  cntrval2  33522  elrgspnlem2  33594  rlocaddval  33620  rlocmulval  33621  idlsrgmulrval  33830  extvval  33952  mplvrpmfgalem  33965  mplvrpmga  33966  mplvrpmmhm  33967  mplvrpmrhm  33968  splyval  33980  issply  33982  esplyval  33983  fedgmul  34052  smatfval  34216  lmatfval  34235  mdetpmtr1  34244  ofcfval  34519  sitmfval  34772  sseqval  34810  sseqf  34814  sseqp1  34817  cndprobval  34855  orvcval  34880  reprval  35029  lpadval  35098  satf  35866  satefv  35927  mclsval  36076  fwddifnval  36676  bj-imdirvallem  37865  finxpreclem1  38076  finxpreclem3  38080  ismtyval  38492  rrnmval  38520  isprimroot  42901  aks6d1c2p2  42927  aks6d1c2lem3  42934  aks6d1c2lem4  42935  aks6d1c6lem3  42980  ovmpogad  43046  tfsconcatun  44105  rfovd  44768  fsovd  44775  fsovrfovd  44776  mnringmulrvald  44992  bccval  45089  fmuldfeqlem1  46339  rrndistlt  47045  hoidmvval  47332  hspval  47364  hoiqssbllem2  47378  smflimlem3  47528  copissgrp  48974  copisnmnd  48975  intopval  49008  cznrng  49067  rngchomALTV  49074  rngccoALTV  49077  funcringcsetcALTV2lem5  49100  ringchomALTV  49108  ringccoALTV  49111  funcringcsetclem5ALTV  49123  srhmsubcALTVlem2  49130  srhmsubcALTV  49131  fldhmsubcALTV  49139  lmod1lem1  49308  lmod1lem2  49309  lmod1lem3  49310  lmod1lem4  49311  lmod1lem5  49312  fdivval  49360  digval  49419  itcoval1  49484  itcoval2  49485  itcoval3  49486  itcovalsucov  49489  ackvalsuc1mpt  49499  rrx2plordisom  49544  sphere  49568  iinfssclem3  49875  swapfval  50081  swapf2vala  50089  fucofvalg  50137  fuco112x  50151  fuco21  50155  fuco22  50158  prcofvalg  50195  prcof2a  50208  prcof2  50209  opf2fval  50224  functhinclem3  50265  incat  50420  lanfval  50432  ranfval  50433  lanval  50438  ranval  50439  crosspdot0i  50686