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

Theorem ovmpt2d 6945
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 2753 . 2 ((𝜑𝑥 = 𝐴) → 𝐷 = 𝐷)
4 ovmpt2d.3 . 2 (𝜑𝐴𝐶)
5 ovmpt2d.4 . 2 (𝜑𝐵𝐷)
6 ovmpt2d.5 . 2 (𝜑𝑆𝑋)
71, 2, 3, 4, 5, 6ovmpt2dx 6944 1 (𝜑 → (𝐴𝐹𝐵) = 𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1624  wcel 2131  (class class class)co 6805  cmpt2 6807
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-sep 4925  ax-nul 4933  ax-pr 5047
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ral 3047  df-rex 3048  df-rab 3051  df-v 3334  df-sbc 3569  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-sn 4314  df-pr 4316  df-op 4320  df-uni 4581  df-br 4797  df-opab 4857  df-id 5166  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-iota 6004  df-fun 6043  df-fv 6049  df-ov 6808  df-oprab 6809  df-mpt2 6810
This theorem is referenced by:  ovmpt2ga  6947  el2mpt2csbcl  7410  suppval  7457  sprmpt2d  7511  mpt2curryd  7556  erov  8003  cnfcomlem  8761  swrdval  13608  splval  13694  0csh0  13731  relexp0g  13953  relexpsucnnr  13956  relexp1g  13957  ramval  15906  prdsval  16309  prdsplusgval  16327  prdsmulrval  16329  prdsdsval  16332  prdsvscaval  16333  imasval  16365  imasdsval  16369  qusval  16396  homfval  16545  comffval  16552  comfval  16553  oppccofval  16569  ismon  16586  sectfval  16604  invfval  16612  cofuval  16735  cofu2nd  16738  resfval  16745  isnat  16800  fucval  16811  fucco  16815  setchom  16923  setcco  16926  catchom  16942  catcco  16944  estrchom  16960  estrcco  16963  funcestrcsetclem5  16977  funcsetcestrclem5  16992  xpcval  17010  xpcid  17022  1stf2  17026  2ndf2  17029  prfval  17032  prf2fval  17034  evlfval  17050  evlf2  17051  evlf2val  17052  evlf1  17053  curfval  17056  uncfval  17067  diagval  17073  hof2fval  17088  hof2val  17089  yonedalem4a  17108  gsumvalx  17463  mgm2nsgrplem2  17599  mgm2nsgrplem3  17600  sgrp2nmndlem2  17604  sgrp2nmndlem3  17605  pj1fval  18299  isrim0  18917  rmodislmodlem  19124  rmodislmod  19125  psrval  19556  frlmphl  20314  uvcfval  20317  mamufval  20385  mamuval  20386  mamufv  20387  matinvgcell  20435  mpt2matmul  20446  mat1ov  20448  dmatval  20492  dmatmulcl  20500  scmatval  20504  scmatscmiddistr  20508  scmatscm  20513  mvmulfval  20542  mvmulval  20543  1mavmul  20548  maducoeval  20639  symgmatr01  20654  gsummatr01lem3  20657  gsummatr01lem4  20658  gsummatr01  20659  cpmat  20708  mat2pmatfval  20722  mat2pmatvalel  20724  mat2pmatmul  20730  cpm2mfval  20748  cpm2mvalel  20750  m2cpminvid  20752  m2cpminvid2  20754  decpmatval0  20763  decpmate  20765  decpmataa0  20767  decpmatmul  20771  pmatcollpw1  20775  monmatcollpw  20778  pmatcollpwlem  20779  pmatcollpw  20780  pmatcollpwscmatlem2  20789  pm2mpval  20794  pm2mpf1  20798  mptcoe1matfsupp  20801  mp2pm2mplem3  20807  mp2pm2mplem4  20808  chmatval  20828  chpmatfval  20829  chp0mat  20845  cnfval  21231  cnpfval  21232  fmval  21940  fmf  21942  fcfval  22030  tsmsval2  22126  blvalps  22383  blval  22384  ishtpy  22964  isphtpy  22973  rrxnm  23371  rrxmval  23380  limcfval  23827  q1pval  24104  r1pval  24107  ismidb  25861  ttgitvval  25953  ebtwntg  26053  ecgrtg  26054  ewlksfval  26699  wwlksn  26932  wwlksnon  26947  wspthsnon  26948  iswwlksnon  26949  iswwlksnonOLD  26950  iswspthsnon  26953  iswspthsnonOLD  26954  clwwlknOLD  27144  numclwlk1lem2  27523  ofoprabco  29765  smatfval  30162  lmatfval  30181  mdetpmtr1  30190  ofcfval  30461  sitmfval  30713  sseqval  30751  sseqf  30755  sseqp1  30758  cndprobval  30796  orvcval  30820  reprval  30989  mclsval  31759  fwddifnval  32568  finxpreclem1  33529  finxpreclem3  33533  ismtyval  33904  rrnmval  33932  rfovd  38789  fsovd  38796  fsovrfovd  38797  bccval  39031  fmuldfeqlem1  40309  rrndistlt  41005  hoidmvval  41289  hspval  41321  hoiqssbllem2  41335  smflimlem3  41479  pfxval  41885  copissgrp  42310  copisnmnd  42311  intopval  42340  rnghmval  42393  isrngisom  42398  rhmval  42421  cznrng  42457  rnghmsscmap2  42475  rnghmsscmap  42476  rngchomALTV  42487  rngccoALTV  42490  funcrngcsetc  42500  funcrngcsetcALT  42501  rhmsscmap2  42521  rhmsscmap  42522  funcringcsetc  42537  funcringcsetcALTV2lem5  42542  ringchomALTV  42550  ringccoALTV  42553  funcringcsetclem5ALTV  42565  srhmsubclem3  42577  srhmsubc  42578  fldhmsubc  42586  srhmsubcALTVlem2  42595  srhmsubcALTV  42596  fldhmsubcALTV  42604  lmod1lem1  42778  lmod1lem2  42779  lmod1lem3  42780  lmod1lem4  42781  lmod1lem5  42782  offval0  42801  fdivval  42835  digval  42894
  Copyright terms: Public domain W3C validator