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

Theorem ovmpt2d 6424
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 2452 . 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 6423 1  |-  ( ph  ->  ( A F B )  =  S )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    = wceq 1444    e. wcel 1887  (class class class)co 6290    |-> cmpt2 6292
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pr 4639
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-sbc 3268  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-br 4403  df-opab 4462  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-iota 5546  df-fun 5584  df-fv 5590  df-ov 6293  df-oprab 6294  df-mpt2 6295
This theorem is referenced by:  ovmpt2ga  6426  suppval  6916  sprmpt2d  6970  mpt2curryd  7016  erov  7460  cnfcomlem  8204  swrdval  12773  splval  12858  0csh0  12895  relexp0g  13085  relexpsucnnr  13088  relexp1g  13089  ramval  14960  ramvalOLD  14961  prdsval  15353  prdsplusgval  15371  prdsmulrval  15373  prdsdsval  15376  prdsvscaval  15377  imasval  15411  imasvalOLD  15412  imasdsval  15416  imasdsvalOLD  15428  qusval  15448  homfval  15597  comffval  15604  comfval  15605  oppccofval  15621  ismon  15638  sectfval  15656  invfval  15664  cofuval  15787  cofu2nd  15790  resfval  15797  isnat  15852  fucval  15863  fucco  15867  setchom  15975  setcco  15978  catchom  15994  catcco  15996  estrchom  16012  estrcco  16015  funcestrcsetclem5  16029  funcsetcestrclem5  16044  xpcval  16062  xpcid  16074  1stf2  16078  2ndf2  16081  prfval  16084  prf2fval  16086  evlfval  16102  evlf2  16103  evlf2val  16104  evlf1  16105  curfval  16108  uncfval  16119  diagval  16125  hof2fval  16140  hof2val  16141  yonedalem4a  16160  gsumvalx  16513  mgm2nsgrplem2  16653  mgm2nsgrplem3  16654  sgrp2nmndlem2  16658  sgrp2nmndlem3  16659  pj1fval  17344  isrim0  17951  psrval  18586  frlmphl  19339  uvcfval  19342  mamufval  19410  mamuval  19411  mamufv  19412  matinvgcell  19460  mpt2matmul  19471  mat1ov  19473  dmatval  19517  dmatmulcl  19525  scmatval  19529  scmatscmiddistr  19533  scmatscm  19538  mvmulfval  19567  mvmulval  19568  1mavmul  19573  maducoeval  19664  symgmatr01  19679  gsummatr01lem3  19682  gsummatr01lem4  19683  gsummatr01  19684  cpmat  19733  mat2pmatfval  19747  mat2pmatvalel  19749  mat2pmatmul  19755  cpm2mfval  19773  cpm2mvalel  19775  m2cpminvid  19777  m2cpminvid2  19779  decpmatval0  19788  decpmate  19790  decpmataa0  19792  decpmatmul  19796  pmatcollpw1  19800  monmatcollpw  19803  pmatcollpwlem  19804  pmatcollpw  19805  pmatcollpwscmatlem2  19814  pm2mpval  19819  pm2mpf1  19823  mptcoe1matfsupp  19826  mp2pm2mplem3  19832  mp2pm2mplem4  19833  chmatval  19853  chpmatfval  19854  chp0mat  19870  cnfval  20249  cnpfval  20250  fmval  20958  fmf  20960  fcfval  21048  tsmsval2  21144  blvalps  21400  blval  21401  ishtpy  22003  isphtpy  22012  rrxnm  22350  rrxmval  22359  limcfval  22827  q1pval  23104  r1pval  23107  ismidb  24820  ttgitvval  24912  ebtwntg  25012  ecgrtg  25013  wlks  25247  trls  25266  pths  25296  spths  25297  wwlk  25409  wwlkn  25410  clwlk  25481  clwwlk  25494  clwwlkn  25495  vdgrfval  25623  iseupa  25693  ofoprabco  28267  smatfval  28621  lmatfval  28640  mdetpmtr1  28649  ofcfval  28919  sitmfval  29183  sseqval  29221  sseqf  29225  sseqp1  29228  cndprobval  29266  orvcval  29290  mclsval  30201  fwddifnval  30930  finxpreclem1  31781  finxpreclem3  31785  ismtyval  32132  rrnmval  32160  bccval  36687  fmuldfeqlem1  37660  rrndistlt  38159  hoidmvval  38399  hspval  38431  hoiqssbllem2  38445  pfxval  38924  ewlksfval  39618  copissgrp  39861  copisnmnd  39862  intopval  39891  rnghmval  39944  isrngisom  39949  rhmval  39972  cznrng  40010  rnghmsscmap2  40028  rnghmsscmap  40029  rngchomALTV  40040  rngccoALTV  40043  funcrngcsetc  40053  funcrngcsetcALT  40054  rhmsscmap2  40074  rhmsscmap  40075  funcringcsetc  40090  funcringcsetcALTV2lem5  40095  ringchomALTV  40103  ringccoALTV  40106  funcringcsetclem5ALTV  40118  srhmsubclem3  40130  srhmsubc  40131  fldhmsubc  40139  srhmsubcALTVlem3  40149  srhmsubcALTV  40150  fldhmsubcALTV  40158  lmod1lem1  40333  lmod1lem2  40334  lmod1lem3  40335  lmod1lem4  40336  lmod1lem5  40337  offval0  40356  fdivval  40403  digval  40462
  Copyright terms: Public domain W3C validator