Theorem ovmpod 7572

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  (class class class)co 7420   ∈ cmpo 7422

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-iota 6494  df-fun 6540  df-fv 6546  df-ov 7423  df-oprab 7424  df-mpo 7425

This theorem is used by:  ovmpoga  7574  fvmpopr2d  7582  elovmpod  7665  el2mpocsbcl  8096  fsplitfpar  8131  suppval  8181  sprmpod  8244  mpocurryd  8289  erov  8838  cnfcomlem  9703  swrdval  14795  pfxval  14827  splval  14904  0csh0  14948  relexp0g  15180  relexpsucnnr  15183  relexp1g  15184  ramval  17191  prdsval  17631  prdsplusgval  17649  prdsmulrval  17651  prdsdsval  17654  prdsvscaval  17655  imasval  17688  imasdsval  17692  qusval  17719  homfval  17871  comffval  17878  comfval  17879  oppccofval  17895  ismon  17913  sectfval  17931  invfval  17939  cofuval  18062  cofu2nd  18065  resfval  18072  isnat  18130  fucval  18141  fucco  18145  setchom  18260  setcco  18263  catchom  18283  catcco  18285  estrchom  18306  estrcco  18309  funcestrcsetclem5  18323  funcsetcestrclem5  18338  xpcval  18356  xpcid  18368  1stf2  18372  2ndf2  18375  prfval  18378  prf2fval  18380  evlfval  18396  evlf2  18397  evlf2val  18398  evlf1  18399  curfval  18402  uncfval  18413  diagval  18419  hof2fval  18434  hof2val  18435  yonedalem4a  18454  gsumvalx  18870  mgm2nsgrplem2  19123  mgm2nsgrplem3  19124  sgrp2nmndlem2  19128  sgrp2nmndlem3  19129  pwmndgplus  19146  symgov  19603  pj1fval  19913  rnghmval  20675  isrngim  20680  isrim0  20718  rhmval  20743  rnghmsscmap2  20886  rnghmsscmap  20887  funcrngcsetc  20897  funcrngcsetcALT  20898  rhmsscmap2  20915  rhmsscmap  20916  funcringcsetc  20931  srhmsubclem3  20936  srhmsubc  20937  fldhmsubc  21047  rmodislmodlem  21209  rmodislmod  21210  frlmphl  22092  uvcfval  22095  psrval  22228  selvffval  22432  psdffval  22483  mamufval  22712  mamuval  22713  mamufv  22714  matinvgcell  22755  mpomatmul  22766  mat1ov  22768  dmatval  22812  dmatmulcl  22820  scmatval  22824  scmatscmiddistr  22828  scmatscm  22833  mvmulfval  22862  mvmulval  22863  1mavmul  22868  maducoeval  22959  symgmatr01  22974  gsummatr01lem3  22977  gsummatr01lem4  22978  gsummatr01  22979  cpmat  23032  mat2pmatfval  23046  mat2pmatvalel  23048  mat2pmatmul  23054  cpm2mfval  23072  cpm2mvalel  23074  m2cpminvid  23076  m2cpminvid2  23078  decpmatval0  23087  decpmate  23089  decpmataa0  23091  decpmatmul  23095  pmatcollpw1  23099  monmatcollpw  23102  pmatcollpwlem  23103  pmatcollpw  23104  pmatcollpwscmatlem2  23113  pm2mpval  23118  pm2mpf1  23122  mptcoe1matfsupp  23125  mp2pm2mplem3  23131  mp2pm2mplem4  23132  chmatval  23152  chpmatfval  23153  chp0mat  23169  cnfval  23556  cnpfval  23557  fmval  24267  fmf  24269  fcfval  24357  tsmsval2  24454  blvalps  24709  blval  24710  ishtpy  25298  isphtpy  25307  rrxnm  25717  rrxmval  25731  rrxdsfival  25739  ehl2eudisval  25749  limcfval  26197  q1pval  26478  r1pval  26481  ismidb  29288  angmgmaddov1  29393  angmgmaddov2  29394  ttgitvval  29464  ebtwntg  29565  ecgrtg  29566  ewlksfval  30187  wwlksnon  30445  wspthsnon  30446  iswwlksnon  30447  iswspthsnon  30450  numclwlk1lem2  30976  ofoprabco  33305  of0r  33320  mntoval  33589  mgcoval  33593  fxpval  33772  conjga  33777  cntrval2  33778  elrgspnlem2  33850  rlocaddval  33876  rlocmulval  33877  idlsrgmulrval  34087  extvval  34209  mplvrpmfgalem  34222  mplvrpmga  34223  mplvrpmmhm  34224  mplvrpmrhm  34225  splyval  34237  issply  34239  esplyval  34240  fedgmul  34309  smatfval  34473  lmatfval  34492  mdetpmtr1  34501  ofcfval  34776  sitmfval  35028  sseqval  35066  sseqf  35070  sseqp1  35073  cndprobval  35111  orvcval  35136  reprval  35285  lpadval  35354  satf  36204  satefv  36265  mclsval  36414  fwddifnval  37020  bj-imdirvallem  38194  finxpreclem1  38405  finxpreclem3  38409  ismtyval  38827  rrnmval  38855  isprimroot  43236  aks6d1c2p2  43262  aks6d1c2lem3  43269  aks6d1c2lem4  43270  aks6d1c6lem3  43315  ovmpogad  43381  tfsconcatun  44432  rfovd  45094  fsovd  45101  fsovrfovd  45102  mnringmulrvald  45318  bccval  45415  fmuldfeqlem1  46687  rrndistlt  47393  hoidmvval  47680  hspval  47712  hoiqssbllem2  47726  smflimlem3  47876  copissgrp  49358  copisnmnd  49359  intopval  49392  cznrng  49451  rngchomALTV  49458  rngccoALTV  49461  funcringcsetcALTV2lem5  49484  ringchomALTV  49492  ringccoALTV  49495  funcringcsetclem5ALTV  49507  srhmsubcALTVlem2  49514  srhmsubcALTV  49515  fldhmsubcALTV  49523  lmod1lem1  49692  lmod1lem2  49693  lmod1lem3  49694  lmod1lem4  49695  lmod1lem5  49696  fdivval  49744  digval  49803  itcoval1  49868  itcoval2  49869  itcoval3  49870  itcovalsucov  49873  ackvalsuc1mpt  49883  rrx2plordisom  49929  sphere  49952  ovmpomptd  50075  iinfssclem3  50263  swapfval  50477  swapf2vala  50485  fucofvalg  50533  fuco112x  50547  fuco21  50551  fuco22  50554  postcof2  50593  prcofvalg  50604  prcof2a  50617  prcof2  50618  opf2fval  50633  functhinclem3  50674  incat  50832  parcoval  50855  lanfval  50889  ranfval  50890  lanval  50895  ranval  50896  crosspdot0lem  51131