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

Theorem ovmpt2d 6830
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 2652 . 2 ((𝜑𝑥 = 𝐴) → 𝐷 = 𝐷)
4 ovmpt2d.3 . 2 (𝜑𝐴𝐶)
5 ovmpt2d.4 . 2 (𝜑𝐵𝐷)
6 ovmpt2d.5 . 2 (𝜑𝑆𝑋)
71, 2, 3, 4, 5, 6ovmpt2dx 6829 1 (𝜑 → (𝐴𝐹𝐵) = 𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1523  wcel 2030  (class class class)co 6690  cmpt2 6692
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-iota 5889  df-fun 5928  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695
This theorem is referenced by:  ovmpt2ga  6832  el2mpt2csbcl  7295  suppval  7342  sprmpt2d  7395  mpt2curryd  7440  erov  7887  cnfcomlem  8634  swrdval  13462  splval  13548  0csh0  13585  relexp0g  13806  relexpsucnnr  13809  relexp1g  13810  ramval  15759  prdsval  16162  prdsplusgval  16180  prdsmulrval  16182  prdsdsval  16185  prdsvscaval  16186  imasval  16218  imasdsval  16222  qusval  16249  homfval  16399  comffval  16406  comfval  16407  oppccofval  16423  ismon  16440  sectfval  16458  invfval  16466  cofuval  16589  cofu2nd  16592  resfval  16599  isnat  16654  fucval  16665  fucco  16669  setchom  16777  setcco  16780  catchom  16796  catcco  16798  estrchom  16814  estrcco  16817  funcestrcsetclem5  16831  funcsetcestrclem5  16846  xpcval  16864  xpcid  16876  1stf2  16880  2ndf2  16883  prfval  16886  prf2fval  16888  evlfval  16904  evlf2  16905  evlf2val  16906  evlf1  16907  curfval  16910  uncfval  16921  diagval  16927  hof2fval  16942  hof2val  16943  yonedalem4a  16962  gsumvalx  17317  mgm2nsgrplem2  17453  mgm2nsgrplem3  17454  sgrp2nmndlem2  17458  sgrp2nmndlem3  17459  pj1fval  18153  isrim0  18771  rmodislmodlem  18978  rmodislmod  18979  psrval  19410  frlmphl  20168  uvcfval  20171  mamufval  20239  mamuval  20240  mamufv  20241  matinvgcell  20289  mpt2matmul  20300  mat1ov  20302  dmatval  20346  dmatmulcl  20354  scmatval  20358  scmatscmiddistr  20362  scmatscm  20367  mvmulfval  20396  mvmulval  20397  1mavmul  20402  maducoeval  20493  symgmatr01  20508  gsummatr01lem3  20511  gsummatr01lem4  20512  gsummatr01  20513  cpmat  20562  mat2pmatfval  20576  mat2pmatvalel  20578  mat2pmatmul  20584  cpm2mfval  20602  cpm2mvalel  20604  m2cpminvid  20606  m2cpminvid2  20608  decpmatval0  20617  decpmate  20619  decpmataa0  20621  decpmatmul  20625  pmatcollpw1  20629  monmatcollpw  20632  pmatcollpwlem  20633  pmatcollpw  20634  pmatcollpwscmatlem2  20643  pm2mpval  20648  pm2mpf1  20652  mptcoe1matfsupp  20655  mp2pm2mplem3  20661  mp2pm2mplem4  20662  chmatval  20682  chpmatfval  20683  chp0mat  20699  cnfval  21085  cnpfval  21086  fmval  21794  fmf  21796  fcfval  21884  tsmsval2  21980  blvalps  22237  blval  22238  ishtpy  22818  isphtpy  22827  rrxnm  23225  rrxmval  23234  limcfval  23681  q1pval  23958  r1pval  23961  ismidb  25715  ttgitvval  25807  ebtwntg  25907  ecgrtg  25908  ewlksfval  26553  wwlksn  26785  wwlksnon  26800  wspthsnon  26801  iswwlksnon  26802  iswwlksnonOLD  26803  iswspthsnon  26806  iswspthsnonOLD  26807  clwwlknOLD  26986  ofoprabco  29592  smatfval  29989  lmatfval  30008  mdetpmtr1  30017  ofcfval  30288  sitmfval  30540  sseqval  30578  sseqf  30582  sseqp1  30585  cndprobval  30623  orvcval  30647  reprval  30816  mclsval  31586  fwddifnval  32395  finxpreclem1  33356  finxpreclem3  33360  ismtyval  33729  rrnmval  33757  rfovd  38612  fsovd  38619  fsovrfovd  38620  bccval  38854  fmuldfeqlem1  40132  rrndistlt  40828  hoidmvval  41112  hspval  41144  hoiqssbllem2  41158  smflimlem3  41302  pfxval  41708  copissgrp  42133  copisnmnd  42134  intopval  42163  rnghmval  42216  isrngisom  42221  rhmval  42244  cznrng  42280  rnghmsscmap2  42298  rnghmsscmap  42299  rngchomALTV  42310  rngccoALTV  42313  funcrngcsetc  42323  funcrngcsetcALT  42324  rhmsscmap2  42344  rhmsscmap  42345  funcringcsetc  42360  funcringcsetcALTV2lem5  42365  ringchomALTV  42373  ringccoALTV  42376  funcringcsetclem5ALTV  42388  srhmsubclem3  42400  srhmsubc  42401  fldhmsubc  42409  srhmsubcALTVlem2  42418  srhmsubcALTV  42419  fldhmsubcALTV  42427  lmod1lem1  42601  lmod1lem2  42602  lmod1lem3  42603  lmod1lem4  42604  lmod1lem5  42605  offval0  42624  fdivval  42658  digval  42717
  Copyright terms: Public domain W3C validator