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

Theorem ovmpt2d 6664
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 2610 . 2 ((𝜑𝑥 = 𝐴) → 𝐷 = 𝐷)
4 ovmpt2d.3 . 2 (𝜑𝐴𝐶)
5 ovmpt2d.4 . 2 (𝜑𝐵𝐷)
6 ovmpt2d.5 . 2 (𝜑𝑆𝑋)
71, 2, 3, 4, 5, 6ovmpt2dx 6663 1 (𝜑 → (𝐴𝐹𝐵) = 𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382   = wceq 1474  wcel 1976  (class class class)co 6527  cmpt2 6529
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pr 4828
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-iota 5754  df-fun 5792  df-fv 5798  df-ov 6530  df-oprab 6531  df-mpt2 6532
This theorem is referenced by:  ovmpt2ga  6666  el2mpt2csbcl  7115  suppval  7162  sprmpt2d  7215  mpt2curryd  7260  erov  7709  cnfcomlem  8457  swrdval  13218  splval  13302  0csh0  13339  relexp0g  13559  relexpsucnnr  13562  relexp1g  13563  ramval  15499  prdsval  15887  prdsplusgval  15905  prdsmulrval  15907  prdsdsval  15910  prdsvscaval  15911  imasval  15943  imasdsval  15947  qusval  15974  homfval  16124  comffval  16131  comfval  16132  oppccofval  16148  ismon  16165  sectfval  16183  invfval  16191  cofuval  16314  cofu2nd  16317  resfval  16324  isnat  16379  fucval  16390  fucco  16394  setchom  16502  setcco  16505  catchom  16521  catcco  16523  estrchom  16539  estrcco  16542  funcestrcsetclem5  16556  funcsetcestrclem5  16571  xpcval  16589  xpcid  16601  1stf2  16605  2ndf2  16608  prfval  16611  prf2fval  16613  evlfval  16629  evlf2  16630  evlf2val  16631  evlf1  16632  curfval  16635  uncfval  16646  diagval  16652  hof2fval  16667  hof2val  16668  yonedalem4a  16687  gsumvalx  17042  mgm2nsgrplem2  17178  mgm2nsgrplem3  17179  sgrp2nmndlem2  17183  sgrp2nmndlem3  17184  pj1fval  17879  isrim0  18495  psrval  19132  frlmphl  19887  uvcfval  19890  mamufval  19958  mamuval  19959  mamufv  19960  matinvgcell  20008  mpt2matmul  20019  mat1ov  20021  dmatval  20065  dmatmulcl  20073  scmatval  20077  scmatscmiddistr  20081  scmatscm  20086  mvmulfval  20115  mvmulval  20116  1mavmul  20121  maducoeval  20212  symgmatr01  20227  gsummatr01lem3  20230  gsummatr01lem4  20231  gsummatr01  20232  cpmat  20281  mat2pmatfval  20295  mat2pmatvalel  20297  mat2pmatmul  20303  cpm2mfval  20321  cpm2mvalel  20323  m2cpminvid  20325  m2cpminvid2  20327  decpmatval0  20336  decpmate  20338  decpmataa0  20340  decpmatmul  20344  pmatcollpw1  20348  monmatcollpw  20351  pmatcollpwlem  20352  pmatcollpw  20353  pmatcollpwscmatlem2  20362  pm2mpval  20367  pm2mpf1  20371  mptcoe1matfsupp  20374  mp2pm2mplem3  20380  mp2pm2mplem4  20381  chmatval  20401  chpmatfval  20402  chp0mat  20418  cnfval  20795  cnpfval  20796  fmval  21505  fmf  21507  fcfval  21595  tsmsval2  21691  blvalps  21948  blval  21949  ishtpy  22527  isphtpy  22536  rrxnm  22932  rrxmval  22941  limcfval  23387  q1pval  23662  r1pval  23665  ismidb  25416  ttgitvval  25508  ebtwntg  25608  ecgrtg  25609  wlks  25841  trls  25860  pths  25890  spths  25891  wwlk  26003  wwlkn  26004  clwlk  26075  clwwlk  26088  clwwlkn  26089  vdgrfval  26216  iseupa  26286  ofoprabco  28681  smatfval  29023  lmatfval  29042  mdetpmtr1  29051  ofcfval  29321  sitmfval  29573  sseqval  29611  sseqf  29615  sseqp1  29618  cndprobval  29656  orvcval  29680  mclsval  30548  fwddifnval  31274  finxpreclem1  32226  finxpreclem3  32230  ismtyval  32593  rrnmval  32621  rfovd  37139  fsovd  37146  fsovrfovd  37147  bccval  37383  fmuldfeqlem1  38473  rrndistlt  39010  hoidmvval  39291  hspval  39323  hoiqssbllem2  39337  smflimlem3  39483  pfxval  40071  ewlksfval  40825  wwlksn  41062  wwlksnon  41071  wspthsnon  41072  iswwlksnon  41073  iswspthsnon  41074  clwwlksn  41211  copissgrp  41620  copisnmnd  41621  intopval  41650  rnghmval  41703  isrngisom  41708  rhmval  41731  cznrng  41769  rnghmsscmap2  41787  rnghmsscmap  41788  rngchomALTV  41799  rngccoALTV  41802  funcrngcsetc  41812  funcrngcsetcALT  41813  rhmsscmap2  41833  rhmsscmap  41834  funcringcsetc  41849  funcringcsetcALTV2lem5  41854  ringchomALTV  41862  ringccoALTV  41865  funcringcsetclem5ALTV  41877  srhmsubclem3  41889  srhmsubc  41890  fldhmsubc  41898  srhmsubcALTVlem3  41908  srhmsubcALTV  41909  fldhmsubcALTV  41917  lmod1lem1  42092  lmod1lem2  42093  lmod1lem3  42094  lmod1lem4  42095  lmod1lem5  42096  offval0  42115  fdivval  42153  digval  42212
  Copyright terms: Public domain W3C validator