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 2421 . 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 370    = wceq 1437    e. wcel 1867  (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 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539  ax-nul 4547  ax-pr 4652
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-rab 2782  df-v 3080  df-sbc 3297  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4214  df-br 4418  df-opab 4476  df-id 4760  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-iota 5556  df-fun 5594  df-fv 5600  df-ov 6299  df-oprab 6300  df-mpt2 6301
This theorem is referenced by:  ovmpt2ga  6431  suppval  6918  sprmpt2d  6969  mpt2curryd  7015  erov  7459  cnfcomlem  8194  swrdval  12747  splval  12832  0csh0  12869  relexp0g  13053  relexpsucnnr  13056  relexp1g  13057  ramval  14912  ramvalOLD  14913  prdsval  15305  prdsplusgval  15323  prdsmulrval  15325  prdsdsval  15328  prdsvscaval  15329  imasval  15361  imasdsval  15365  qusval  15392  homfval  15541  comffval  15548  comfval  15549  oppccofval  15565  ismon  15582  sectfval  15600  invfval  15608  cofuval  15731  cofu2nd  15734  resfval  15741  isnat  15796  fucval  15807  fucco  15811  setchom  15919  setcco  15922  catchom  15938  catcco  15940  estrchom  15956  estrcco  15959  funcestrcsetclem5  15973  funcsetcestrclem5  15988  xpcval  16006  xpcid  16018  1stf2  16022  2ndf2  16025  prfval  16028  prf2fval  16030  evlfval  16046  evlf2  16047  evlf2val  16048  evlf1  16049  curfval  16052  uncfval  16063  diagval  16069  hof2fval  16084  hof2val  16085  yonedalem4a  16104  gsumvalx  16457  mgm2nsgrplem2  16597  mgm2nsgrplem3  16598  sgrp2nmndlem2  16602  sgrp2nmndlem3  16603  pj1fval  17272  isrim0  17879  psrval  18514  frlmphl  19263  uvcfval  19266  mamufval  19334  mamuval  19335  mamufv  19336  matinvgcell  19384  mpt2matmul  19395  mat1ov  19397  dmatval  19441  dmatmulcl  19449  scmatval  19453  scmatscmiddistr  19457  scmatscm  19462  mvmulfval  19491  mvmulval  19492  1mavmul  19497  maducoeval  19588  symgmatr01  19603  gsummatr01lem3  19606  gsummatr01lem4  19607  gsummatr01  19608  cpmat  19657  mat2pmatfval  19671  mat2pmatvalel  19673  mat2pmatmul  19679  cpm2mfval  19697  cpm2mvalel  19699  m2cpminvid  19701  m2cpminvid2  19703  decpmatval0  19712  decpmate  19714  decpmataa0  19716  decpmatmul  19720  pmatcollpw1  19724  monmatcollpw  19727  pmatcollpwlem  19728  pmatcollpw  19729  pmatcollpwscmatlem2  19738  pm2mpval  19743  pm2mpf1  19747  mptcoe1matfsupp  19750  mp2pm2mplem3  19756  mp2pm2mplem4  19757  chmatval  19777  chpmatfval  19778  chp0mat  19794  cnfval  20173  cnpfval  20174  fmval  20882  fmf  20884  fcfval  20972  tsmsval2  21068  blvalps  21324  blval  21325  ishtpy  21889  isphtpy  21898  rrxnm  22236  rrxmval  22245  limcfval  22701  q1pval  22976  r1pval  22979  ismidb  24673  ttgitvval  24755  ebtwntg  24855  ecgrtg  24856  wlks  25089  trls  25108  pths  25138  spths  25139  wwlk  25251  wwlkn  25252  clwlk  25323  clwwlk  25336  clwwlkn  25337  vdgrfval  25465  iseupa  25535  ofoprabco  28104  smatfval  28457  lmatfval  28476  mdetpmtr1  28485  ofcfval  28755  sitmfval  29008  sseqval  29044  sseqf  29048  sseqp1  29051  cndprobval  29089  orvcval  29113  mclsval  29986  fwddifnval  30712  ismtyval  31836  rrnmval  31864  bccval  36328  fmuldfeqlem1  37236  pfxval  38327  copissgrp  38579  copisnmnd  38580  intopval  38609  rnghmval  38662  isrngisom  38667  rhmval  38690  cznrng  38728  rnghmsscmap2  38746  rnghmsscmap  38747  rngchomALTV  38758  rngccoALTV  38761  funcrngcsetc  38771  funcrngcsetcALT  38772  rhmsscmap2  38792  rhmsscmap  38793  funcringcsetc  38808  funcringcsetcALTV2lem5  38813  ringchomALTV  38821  ringccoALTV  38824  funcringcsetclem5ALTV  38836  srhmsubclem3  38848  srhmsubc  38849  fldhmsubc  38857  srhmsubcALTVlem3  38867  srhmsubcALTV  38868  fldhmsubcALTV  38876  lmod1lem1  39053  lmod1lem2  39054  lmod1lem3  39055  lmod1lem4  39056  lmod1lem5  39057  offval0  39076  fdivval  39124  digval  39183
  Copyright terms: Public domain W3C validator