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

Theorem ovmpt2d 6142
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 2390 . 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 6141 1  |-  ( ph  ->  ( A F B )  =  S )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649    e. wcel 1717  (class class class)co 6022    e. cmpt2 6024
This theorem is referenced by:  ovmpt2ga  6144  sprmpt2  6414  erov  6939  cnfcomlem  7591  swrdval  11693  splval  11709  ramval  13305  prdsval  13607  prdsplusgval  13624  prdsmulrval  13626  prdsdsval  13629  prdsvscaval  13630  imasval  13666  imasdsval  13670  divsval  13696  homfval  13847  comffval  13854  comfval  13855  oppccofval  13871  ismon  13888  sectfval  13906  invfval  13913  cofuval  14008  cofu2nd  14011  resfval  14018  isnat  14073  fucval  14084  fucco  14088  setchom  14164  setcco  14167  catchom  14183  catcco  14185  xpcval  14203  xpcid  14215  1stf2  14219  2ndf2  14222  prfval  14225  prf2fval  14227  evlfval  14243  evlf2  14244  evlf2val  14245  evlf1  14246  curfval  14249  uncfval  14260  diagval  14266  hof2fval  14281  hof2val  14282  yonedalem4a  14301  gsumvalx  14703  pj1fval  15255  psrval  16358  cnfval  17221  cnpfval  17222  fmval  17898  fmf  17900  fcfval  17988  tsmsval2  18082  blval  18324  ishtpy  18870  isphtpy  18879  limcfval  19628  q1pval  19945  r1pval  19948  wlks  21392  trls  21402  pths  21422  spths  21423  vdgrfval  21516  iseupa  21537  ofoprabco  23923  ofcfval  24279  cndprobval  24472  orvcval  24496  relexp0  24910  relexpsucr  24911  itg2addnclem  25959  itg2addnc  25961  ismtyval  26202  rrnmval  26230  uvcfval  26904  mamufval  27114  mamuval  27115  mamufv  27116  fmuldfeqlem1  27382
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370  ax-sep 4273  ax-nul 4281  ax-pr 4346
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2244  df-mo 2245  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ne 2554  df-ral 2656  df-rex 2657  df-rab 2660  df-v 2903  df-sbc 3107  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-nul 3574  df-if 3685  df-sn 3765  df-pr 3766  df-op 3768  df-uni 3960  df-br 4156  df-opab 4210  df-id 4441  df-xp 4826  df-rel 4827  df-cnv 4828  df-co 4829  df-dm 4830  df-iota 5360  df-fun 5398  df-fv 5404  df-ov 6025  df-oprab 6026  df-mpt2 6027
  Copyright terms: Public domain W3C validator