MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ovmpt2d Structured version   Visualization version   GIF version

Theorem ovmpt2d 7028
Description: Value of an operation given by a maps-to rule, deduction form. (Contributed by Mario Carneiro, 7-Dec-2014.)
Hypotheses
Ref Expression
ovmpt2d.1 (𝜑𝐹 = (𝑥𝐶, 𝑦𝐷𝑅))
ovmpt2d.2 ((𝜑 ∧ (𝑥 = 𝐴𝑦 = 𝐵)) → 𝑅 = 𝑆)
ovmpt2d.3 (𝜑𝐴𝐶)
ovmpt2d.4 (𝜑𝐵𝐷)
ovmpt2d.5 (𝜑𝑆𝑋)
Assertion
Ref Expression
ovmpt2d (𝜑 → (𝐴𝐹𝐵) = 𝑆)
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝑆,𝑦   𝜑,𝑥,𝑦
Allowed substitution hints:   𝐶(𝑥,𝑦)   𝐷(𝑥,𝑦)   𝑅(𝑥,𝑦)   𝐹(𝑥,𝑦)   𝑋(𝑥,𝑦)

Proof of Theorem ovmpt2d
StepHypRef Expression
1 ovmpt2d.1 . 2 (𝜑𝐹 = (𝑥𝐶, 𝑦𝐷𝑅))
2 ovmpt2d.2 . 2 ((𝜑 ∧ (𝑥 = 𝐴𝑦 = 𝐵)) → 𝑅 = 𝑆)
3 eqidd 2818 . 2 ((𝜑𝑥 = 𝐴) → 𝐷 = 𝐷)
4 ovmpt2d.3 . 2 (𝜑𝐴𝐶)
5 ovmpt2d.4 . 2 (𝜑𝐵𝐷)
6 ovmpt2d.5 . 2 (𝜑𝑆𝑋)
71, 2, 3, 4, 5, 6ovmpt2dx 7027 1 (𝜑 → (𝐴𝐹𝐵) = 𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1637  wcel 2157  (class class class)co 6884  cmpt2 6886
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-sep 4988  ax-nul 4996  ax-pr 5109
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3404  df-sbc 3645  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-sn 4382  df-pr 4384  df-op 4388  df-uni 4642  df-br 4856  df-opab 4918  df-id 5232  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-iota 6074  df-fun 6113  df-fv 6119  df-ov 6887  df-oprab 6888  df-mpt2 6889
This theorem is referenced by:  ovmpt2ga  7030  el2mpt2csbcl  7493  suppval  7541  sprmpt2d  7595  mpt2curryd  7640  erov  8090  cnfcomlem  8853  swrdval  13660  splval  13746  0csh0  13783  relexp0g  14005  relexpsucnnr  14008  relexp1g  14009  ramval  15949  prdsval  16340  prdsplusgval  16358  prdsmulrval  16360  prdsdsval  16363  prdsvscaval  16364  imasval  16396  imasdsval  16400  qusval  16427  homfval  16576  comffval  16583  comfval  16584  oppccofval  16600  ismon  16617  sectfval  16635  invfval  16643  cofuval  16766  cofu2nd  16769  resfval  16776  isnat  16831  fucval  16842  fucco  16846  setchom  16954  setcco  16957  catchom  16973  catcco  16975  estrchom  16991  estrcco  16994  funcestrcsetclem5  17009  funcsetcestrclem5  17024  xpcval  17042  xpcid  17054  1stf2  17058  2ndf2  17061  prfval  17064  prf2fval  17066  evlfval  17082  evlf2  17083  evlf2val  17084  evlf1  17085  curfval  17088  uncfval  17099  diagval  17105  hof2fval  17120  hof2val  17121  yonedalem4a  17140  gsumvalx  17495  mgm2nsgrplem2  17631  mgm2nsgrplem3  17632  sgrp2nmndlem2  17636  sgrp2nmndlem3  17637  pj1fval  18328  isrim0  18947  rmodislmodlem  19154  rmodislmod  19155  psrval  19591  frlmphl  20351  uvcfval  20354  mamufval  20422  mamuval  20423  mamufv  20424  matinvgcell  20472  mpt2matmul  20484  mat1ov  20486  dmatval  20530  dmatmulcl  20538  scmatval  20542  scmatscmiddistr  20546  scmatscm  20551  mvmulfval  20580  mvmulval  20581  1mavmul  20586  maducoeval  20677  symgmatr01  20693  gsummatr01lem3  20696  gsummatr01lem4  20697  gsummatr01  20698  cpmat  20748  mat2pmatfval  20762  mat2pmatvalel  20764  mat2pmatmul  20770  cpm2mfval  20788  cpm2mvalel  20790  m2cpminvid  20792  m2cpminvid2  20794  decpmatval0  20803  decpmate  20805  decpmataa0  20807  decpmatmul  20811  pmatcollpw1  20815  monmatcollpw  20818  pmatcollpwlem  20819  pmatcollpw  20820  pmatcollpwscmatlem2  20829  pm2mpval  20834  pm2mpf1  20838  mptcoe1matfsupp  20841  mp2pm2mplem3  20847  mp2pm2mplem4  20848  chmatval  20868  chpmatfval  20869  chp0mat  20885  cnfval  21272  cnpfval  21273  fmval  21981  fmf  21983  fcfval  22071  tsmsval2  22167  blvalps  22424  blval  22425  ishtpy  23005  isphtpy  23014  rrxnm  23414  rrxmval  23423  limcfval  23873  q1pval  24150  r1pval  24153  ismidb  25907  ttgitvval  25999  ebtwntg  26099  ecgrtg  26100  ewlksfval  26748  wwlksn  26981  wwlksnon  26996  wspthsnon  26997  iswwlksnon  26998  iswwlksnonOLD  26999  iswspthsnon  27002  iswspthsnonOLD  27003  clwwlknOLD  27195  numclwlk1lem2  27573  ofoprabco  29814  smatfval  30209  lmatfval  30228  mdetpmtr1  30237  ofcfval  30508  sitmfval  30760  sseqval  30798  sseqf  30802  sseqp1  30805  cndprobval  30843  orvcval  30867  reprval  31036  mclsval  31805  fwddifnval  32613  finxpreclem1  33561  finxpreclem3  33565  ismtyval  33929  rrnmval  33957  rfovd  38813  fsovd  38820  fsovrfovd  38821  bccval  39055  fmuldfeqlem1  40312  rrndistlt  41007  hoidmvval  41291  hspval  41323  hoiqssbllem2  41337  smflimlem3  41481  pfxval  41976  copissgrp  42394  copisnmnd  42395  intopval  42424  rnghmval  42477  isrngisom  42482  rhmval  42505  cznrng  42541  rnghmsscmap2  42559  rnghmsscmap  42560  rngchomALTV  42571  rngccoALTV  42574  funcrngcsetc  42584  funcrngcsetcALT  42585  rhmsscmap2  42605  rhmsscmap  42606  funcringcsetc  42621  funcringcsetcALTV2lem5  42626  ringchomALTV  42634  ringccoALTV  42637  funcringcsetclem5ALTV  42649  srhmsubclem3  42661  srhmsubc  42662  fldhmsubc  42670  srhmsubcALTVlem2  42679  srhmsubcALTV  42680  fldhmsubcALTV  42688  lmod1lem1  42862  lmod1lem2  42863  lmod1lem3  42864  lmod1lem4  42865  lmod1lem5  42866  offval0  42885  fdivval  42919  digval  42978
  Copyright terms: Public domain W3C validator