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

Theorem ovmpt2d 6686
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 2611 . 2 ((𝜑𝑥 = 𝐴) → 𝐷 = 𝐷)
4 ovmpt2d.3 . 2 (𝜑𝐴𝐶)
5 ovmpt2d.4 . 2 (𝜑𝐵𝐷)
6 ovmpt2d.5 . 2 (𝜑𝑆𝑋)
71, 2, 3, 4, 5, 6ovmpt2dx 6685 1 (𝜑 → (𝐴𝐹𝐵) = 𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1475  wcel 1977  (class class class)co 6549  cmpt2 6551
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-iota 5768  df-fun 5806  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554
This theorem is referenced by:  ovmpt2ga  6688  el2mpt2csbcl  7137  suppval  7184  sprmpt2d  7237  mpt2curryd  7282  erov  7731  cnfcomlem  8479  swrdval  13269  splval  13353  0csh0  13390  relexp0g  13610  relexpsucnnr  13613  relexp1g  13614  ramval  15550  prdsval  15938  prdsplusgval  15956  prdsmulrval  15958  prdsdsval  15961  prdsvscaval  15962  imasval  15994  imasdsval  15998  qusval  16025  homfval  16175  comffval  16182  comfval  16183  oppccofval  16199  ismon  16216  sectfval  16234  invfval  16242  cofuval  16365  cofu2nd  16368  resfval  16375  isnat  16430  fucval  16441  fucco  16445  setchom  16553  setcco  16556  catchom  16572  catcco  16574  estrchom  16590  estrcco  16593  funcestrcsetclem5  16607  funcsetcestrclem5  16622  xpcval  16640  xpcid  16652  1stf2  16656  2ndf2  16659  prfval  16662  prf2fval  16664  evlfval  16680  evlf2  16681  evlf2val  16682  evlf1  16683  curfval  16686  uncfval  16697  diagval  16703  hof2fval  16718  hof2val  16719  yonedalem4a  16738  gsumvalx  17093  mgm2nsgrplem2  17229  mgm2nsgrplem3  17230  sgrp2nmndlem2  17234  sgrp2nmndlem3  17235  pj1fval  17930  isrim0  18546  psrval  19183  frlmphl  19939  uvcfval  19942  mamufval  20010  mamuval  20011  mamufv  20012  matinvgcell  20060  mpt2matmul  20071  mat1ov  20073  dmatval  20117  dmatmulcl  20125  scmatval  20129  scmatscmiddistr  20133  scmatscm  20138  mvmulfval  20167  mvmulval  20168  1mavmul  20173  maducoeval  20264  symgmatr01  20279  gsummatr01lem3  20282  gsummatr01lem4  20283  gsummatr01  20284  cpmat  20333  mat2pmatfval  20347  mat2pmatvalel  20349  mat2pmatmul  20355  cpm2mfval  20373  cpm2mvalel  20375  m2cpminvid  20377  m2cpminvid2  20379  decpmatval0  20388  decpmate  20390  decpmataa0  20392  decpmatmul  20396  pmatcollpw1  20400  monmatcollpw  20403  pmatcollpwlem  20404  pmatcollpw  20405  pmatcollpwscmatlem2  20414  pm2mpval  20419  pm2mpf1  20423  mptcoe1matfsupp  20426  mp2pm2mplem3  20432  mp2pm2mplem4  20433  chmatval  20453  chpmatfval  20454  chp0mat  20470  cnfval  20847  cnpfval  20848  fmval  21557  fmf  21559  fcfval  21647  tsmsval2  21743  blvalps  22000  blval  22001  ishtpy  22579  isphtpy  22588  rrxnm  22987  rrxmval  22996  limcfval  23442  q1pval  23717  r1pval  23720  ismidb  25470  ttgitvval  25562  ebtwntg  25662  ecgrtg  25663  wlks  26047  trls  26066  pths  26096  spths  26097  wwlk  26209  wwlkn  26210  clwlk  26281  clwwlk  26294  clwwlkn  26295  vdgrfval  26422  iseupa  26492  ofoprabco  28847  smatfval  29189  lmatfval  29208  mdetpmtr1  29217  ofcfval  29487  sitmfval  29739  sseqval  29777  sseqf  29781  sseqp1  29784  cndprobval  29822  orvcval  29846  mclsval  30714  fwddifnval  31440  finxpreclem1  32402  finxpreclem3  32406  ismtyval  32769  rrnmval  32797  rfovd  37315  fsovd  37322  fsovrfovd  37323  bccval  37559  fmuldfeqlem1  38649  rrndistlt  39186  hoidmvval  39467  hspval  39499  hoiqssbllem2  39513  smflimlem3  39659  pfxval  40246  ewlksfval  40803  wwlksn  41040  wwlksnon  41049  wspthsnon  41050  iswwlksnon  41051  iswspthsnon  41052  clwwlksn  41189  copissgrp  41598  copisnmnd  41599  intopval  41628  rnghmval  41681  isrngisom  41686  rhmval  41709  cznrng  41747  rnghmsscmap2  41765  rnghmsscmap  41766  rngchomALTV  41777  rngccoALTV  41780  funcrngcsetc  41790  funcrngcsetcALT  41791  rhmsscmap2  41811  rhmsscmap  41812  funcringcsetc  41827  funcringcsetcALTV2lem5  41832  ringchomALTV  41840  ringccoALTV  41843  funcringcsetclem5ALTV  41855  srhmsubclem3  41867  srhmsubc  41868  fldhmsubc  41876  srhmsubcALTVlem3  41886  srhmsubcALTV  41887  fldhmsubcALTV  41895  lmod1lem1  42070  lmod1lem2  42071  lmod1lem3  42072  lmod1lem4  42073  lmod1lem5  42074  offval0  42093  fdivval  42131  digval  42190
  Copyright terms: Public domain W3C validator