Theorem ovmpod 7599

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147  (class class class)co 7446   ∈ cmpo 7448

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-pr 5396

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5172  df-id 5551  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-iota 6515  df-fun 6563  df-fv 6569  df-ov 7449  df-oprab 7450  df-mpo 7451

This theorem is used by:  ovmpoga  7601  fvmpopr2d  7609  elovmpod  7692  el2mpocsbcl  8124  fsplitfpar  8159  suppval  8209  sprmpod  8272  mpocurryd  8317  erov  8866  cnfcomlem  9730  swrdval  14822  pfxval  14854  splval  14931  0csh0  14975  relexp0g  15207  relexpsucnnr  15210  relexp1g  15211  ramval  17218  prdsval  17658  prdsplusgval  17676  prdsmulrval  17678  prdsdsval  17681  prdsvscaval  17682  imasval  17715  imasdsval  17719  qusval  17746  homfval  17898  comffval  17905  comfval  17906  oppccofval  17922  ismon  17940  sectfval  17958  invfval  17966  cofuval  18089  cofu2nd  18092  resfval  18099  isnat  18157  fucval  18168  fucco  18172  setchom  18287  setcco  18290  catchom  18310  catcco  18312  estrchom  18333  estrcco  18336  funcestrcsetclem5  18350  funcsetcestrclem5  18365  xpcval  18383  xpcid  18395  1stf2  18399  2ndf2  18402  prfval  18405  prf2fval  18407  evlfval  18423  evlf2  18424  evlf2val  18425  evlf1  18426  curfval  18429  uncfval  18440  diagval  18446  hof2fval  18461  hof2val  18462  yonedalem4a  18481  gsumvalx  18897  mgm2nsgrplem2  19150  mgm2nsgrplem3  19151  sgrp2nmndlem2  19155  sgrp2nmndlem3  19156  pwmndgplus  19173  symgov  19631  pj1fval  19941  rnghmval  20703  isrngim  20708  isrim0  20746  rhmval  20771  rnghmsscmap2  20914  rnghmsscmap  20915  funcrngcsetc  20925  funcrngcsetcALT  20926  rhmsscmap2  20943  rhmsscmap  20944  funcringcsetc  20959  srhmsubclem3  20964  srhmsubc  20965  fldhmsubc  21075  rmodislmodlem  21237  rmodislmod  21238  frlmphl  22120  uvcfval  22123  psrval  22256  selvffval  22460  psdffval  22511  mamufval  22740  mamuval  22741  mamufv  22742  matinvgcell  22783  mpomatmul  22794  mat1ov  22796  dmatval  22840  dmatmulcl  22848  scmatval  22852  scmatscmiddistr  22856  scmatscm  22861  mvmulfval  22890  mvmulval  22891  1mavmul  22896  maducoeval  22987  symgmatr01  23002  gsummatr01lem3  23005  gsummatr01lem4  23006  gsummatr01  23007  cpmat  23060  mat2pmatfval  23074  mat2pmatvalel  23076  mat2pmatmul  23082  cpm2mfval  23100  cpm2mvalel  23102  m2cpminvid  23104  m2cpminvid2  23106  decpmatval0  23115  decpmate  23117  decpmataa0  23119  decpmatmul  23123  pmatcollpw1  23127  monmatcollpw  23130  pmatcollpwlem  23131  pmatcollpw  23132  pmatcollpwscmatlem2  23141  pm2mpval  23146  pm2mpf1  23150  mptcoe1matfsupp  23153  mp2pm2mplem3  23159  mp2pm2mplem4  23160  chmatval  23180  chpmatfval  23181  chp0mat  23197  cnfval  23584  cnpfval  23585  fmval  24295  fmf  24297  fcfval  24385  tsmsval2  24482  blvalps  24737  blval  24738  ishtpy  25326  isphtpy  25335  rrxnm  25745  rrxmval  25759  rrxdsfival  25767  ehl2eudisval  25777  limcfval  26225  q1pval  26506  r1pval  26509  ismidb  29316  angmgmaddov1  29421  angmgmaddov2  29422  ttgitvval  29492  ebtwntg  29593  ecgrtg  29594  ewlksfval  30215  wwlksnon  30473  wspthsnon  30474  iswwlksnon  30475  iswspthsnon  30478  numclwlk1lem2  31004  ofoprabco  33333  of0r  33347  mntoval  33619  mgcoval  33623  fxpval  33802  conjga  33807  cntrval2  33808  elrgspnlem2  33880  rlocaddval  33906  rlocmulval  33907  idlsrgmulrval  34125  extvval  34246  mplvrpmfgalem  34259  mplvrpmga  34260  mplvrpmmhm  34261  mplvrpmrhm  34262  splyval  34274  issply  34276  esplyval  34277  fedgmul  34346  smatfval  34510  lmatfval  34529  mdetpmtr1  34538  ofcfval  34813  sitmfval  35065  sseqval  35103  sseqf  35107  sseqp1  35110  cndprobval  35148  orvcval  35173  reprval  35322  lpadval  35391  satf  36298  satefv  36359  mclsval  36508  fwddifnval  37119  bj-imdirvallem  38306  finxpreclem1  38517  finxpreclem3  38521  ismtyval  38937  rrnmval  38965  isprimroot  43346  aks6d1c2p2  43372  aks6d1c2lem3  43379  aks6d1c2lem4  43380  aks6d1c6lem3  43425  ovmpogad  43492  tfsconcatun  44542  rfovd  45204  fsovd  45211  fsovrfovd  45212  mnringmulrvald  45428  bccval  45525  fmuldfeqlem1  46809  rrndistlt  47515  hoidmvval  47802  hspval  47834  hoiqssbllem2  47848  smflimlem3  47998  copissgrp  49480  copisnmnd  49481  intopval  49514  cznrng  49573  rngchomALTV  49580  rngccoALTV  49583  funcringcsetcALTV2lem5  49606  ringchomALTV  49614  ringccoALTV  49617  funcringcsetclem5ALTV  49629  srhmsubcALTVlem2  49636  srhmsubcALTV  49637  fldhmsubcALTV  49645  lmod1lem1  49814  lmod1lem2  49815  lmod1lem3  49816  lmod1lem4  49817  lmod1lem5  49818  fdivval  49866  digval  49925  itcoval1  49990  itcoval2  49991  itcoval3  49992  itcovalsucov  49995  ackvalsuc1mpt  50005  rrx2plordisom  50051  sphere  50074  ovmpomptd  50197  iinfssclem3  50385  swapfval  50599  swapf2vala  50607  fucofvalg  50655  fuco112x  50669  fuco21  50673  fuco22  50676  postcof2  50715  prcofvalg  50726  prcof2a  50739  prcof2  50740  opf2fval  50755  functhinclem3  50796  incat  50954  parcoval  50977  lanfval  51011  ranfval  51012  lanval  51017  ranval  51018  crosspdot0lem  51275