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

Theorem ovmpt2d 6429
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  |-  ( ph  ->  F  =  ( x  e.  C ,  y  e.  D  |->  R ) )
ovmpt2d.2  |-  ( (
ph  /\  ( x  =  A  /\  y  =  B ) )  ->  R  =  S )
ovmpt2d.3  |-  ( ph  ->  A  e.  C )
ovmpt2d.4  |-  ( ph  ->  B  e.  D )
ovmpt2d.5  |-  ( ph  ->  S  e.  X )
Assertion
Ref Expression
ovmpt2d  |-  ( ph  ->  ( A F B )  =  S )
Distinct variable groups:    x, y, A    x, B, y    x, S, y    ph, x, y
Allowed substitution hints:    C( x, y)    D( x, y)    R( x, y)    F( x, y)    X( x, y)

Proof of Theorem ovmpt2d
StepHypRef Expression
1 ovmpt2d.1 . 2  |-  ( ph  ->  F  =  ( x  e.  C ,  y  e.  D  |->  R ) )
2 ovmpt2d.2 . 2  |-  ( (
ph  /\  ( x  =  A  /\  y  =  B ) )  ->  R  =  S )
3 eqidd 2458 . 2  |-  ( (
ph  /\  x  =  A )  ->  D  =  D )
4 ovmpt2d.3 . 2  |-  ( ph  ->  A  e.  C )
5 ovmpt2d.4 . 2  |-  ( ph  ->  B  e.  D )
6 ovmpt2d.5 . 2  |-  ( ph  ->  S  e.  X )
71, 2, 3, 4, 5, 6ovmpt2dx 6428 1  |-  ( ph  ->  ( A F B )  =  S )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1395    e. wcel 1819  (class class class)co 6296    |-> cmpt2 6298
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pr 4695
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-br 4457  df-opab 4516  df-id 4804  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-iota 5557  df-fun 5596  df-fv 5602  df-ov 6299  df-oprab 6300  df-mpt2 6301
This theorem is referenced by:  ovmpt2ga  6431  suppval  6919  sprmpt2d  6970  mpt2curryd  7016  erov  7426  cnfcomlem  8160  cnfcomlemOLD  8168  swrdval  12652  splval  12738  0csh0  12775  ramval  14537  prdsval  14871  prdsplusgval  14889  prdsmulrval  14891  prdsdsval  14894  prdsvscaval  14895  imasval  14927  imasdsval  14931  qusval  14958  homfval  15107  comffval  15114  comfval  15115  oppccofval  15131  ismon  15148  sectfval  15166  invfval  15174  cofuval  15297  cofu2nd  15300  resfval  15307  isnat  15362  fucval  15373  fucco  15377  setchom  15485  setcco  15488  catchom  15504  catcco  15506  estrchom  15522  estrcco  15525  funcestrcsetclem5  15539  funcsetcestrclem5  15554  xpcval  15572  xpcid  15584  1stf2  15588  2ndf2  15591  prfval  15594  prf2fval  15596  evlfval  15612  evlf2  15613  evlf2val  15614  evlf1  15615  curfval  15618  uncfval  15629  diagval  15635  hof2fval  15650  hof2val  15651  yonedalem4a  15670  gsumvalx  16023  mgm2nsgrplem2  16163  mgm2nsgrplem3  16164  sgrp2nmndlem2  16168  sgrp2nmndlem3  16169  pj1fval  16838  isrim0  17498  psrval  18137  frlmphl  18938  uvcfval  18941  mamufval  19013  mamuval  19014  mamufv  19015  matinvgcell  19063  mpt2matmul  19074  mat1ov  19076  dmatval  19120  dmatmulcl  19128  scmatval  19132  scmatscmiddistr  19136  scmatscm  19141  mvmulfval  19170  mvmulval  19171  1mavmul  19176  maducoeval  19267  symgmatr01  19282  gsummatr01lem3  19285  gsummatr01lem4  19286  gsummatr01  19287  cpmat  19336  mat2pmatfval  19350  mat2pmatvalel  19352  mat2pmatmul  19358  cpm2mfval  19376  cpm2mvalel  19378  m2cpminvid  19380  m2cpminvid2  19382  decpmatval0  19391  decpmate  19393  decpmataa0  19395  decpmatmul  19399  pmatcollpw1  19403  monmatcollpw  19406  pmatcollpwlem  19407  pmatcollpw  19408  pmatcollpwscmatlem2  19417  pm2mpval  19422  pm2mpf1  19426  mptcoe1matfsupp  19429  mp2pm2mplem3  19435  mp2pm2mplem4  19436  chmatval  19456  chpmatfval  19457  chp0mat  19473  cnfval  19860  cnpfval  19861  fmval  20569  fmf  20571  fcfval  20659  tsmsval2  20753  blvalps  21013  blval  21014  ishtpy  21597  isphtpy  21606  rrxnm  21948  rrxmval  21957  limcfval  22401  q1pval  22679  r1pval  22682  ismidb  24269  ttgitvval  24311  ebtwntg  24411  ecgrtg  24412  wlks  24645  trls  24664  pths  24694  spths  24695  wwlk  24807  wwlkn  24808  clwlk  24879  clwwlk  24892  clwwlkn  24893  vdgrfval  25021  iseupa  25091  ofoprabco  27653  ofcfval  28258  sitmfval  28466  sseqval  28502  sseqf  28506  sseqp1  28509  cndprobval  28547  orvcval  28571  mclsval  29098  relexp0  29227  relexpsucr  29228  ismtyval  30458  rrnmval  30486  bccval  31405  fmuldfeqlem1  31737  pfxval  32458  copissgrp  32716  copisnmnd  32717  intopval  32746  rnghmval  32799  isrngisom  32804  rhmval  32827  cznrng  32865  rnghmsscmap2  32883  rnghmsscmap  32884  rngchomOLD  32895  rngccoOLD  32898  funcrngcsetc  32908  funcrngcsetcALT  32909  rhmsscmap2  32929  rhmsscmap  32930  funcringcsetc  32945  funcringcsetcOLD2lem5  32950  ringchomOLD  32958  ringccoOLD  32961  funcringcsetclem5OLD  32973  srhmsubclem3  32985  srhmsubc  32986  fldhmsubc  32994  srhmsubcOLDlem3  33004  srhmsubcOLD  33005  fldhmsubcOLD  33013  lmod1lem1  33190  lmod1lem2  33191  lmod1lem3  33192  lmod1lem4  33193  lmod1lem5  33194
  Copyright terms: Public domain W3C validator