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

Theorem ovmpt2d 5991
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 2297 . 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 5990 1  |-  ( ph  ->  ( A F B )  =  S )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1632    e. wcel 1696  (class class class)co 5874    e. cmpt2 5876
This theorem is referenced by:  ovmpt2ga  5993  erov  6771  cnfcomlem  7418  swrdval  11466  splval  11482  ramval  13071  prdsval  13371  prdsplusgval  13388  prdsmulrval  13390  prdsdsval  13393  prdsvscaval  13394  imasval  13430  imasdsval  13434  divsval  13460  homfval  13611  comffval  13618  comfval  13619  oppccofval  13635  ismon  13652  sectfval  13670  invfval  13677  cofuval  13772  cofu2nd  13775  resfval  13782  isnat  13837  fucval  13848  fucco  13852  setchom  13928  setcco  13931  catchom  13947  catcco  13949  xpcval  13967  xpcid  13979  1stf2  13983  2ndf2  13986  prfval  13989  prf2fval  13991  evlfval  14007  evlf2  14008  evlf2val  14009  evlf1  14010  curfval  14013  uncfval  14024  diagval  14030  hof2fval  14045  hof2val  14046  yonedalem4a  14065  gsumvalx  14467  pj1fval  15019  psrval  16126  cnfval  16979  cnpfval  16980  fmval  17654  fmf  17656  fcfval  17744  tsmsval2  17828  blval  17964  ishtpy  18486  isphtpy  18495  limcfval  19238  q1pval  19555  r1pval  19558  ofoprabco  23247  ofcfval  23474  cndprobval  23651  orvcval  23673  iseupa  23896  vdgrfval  23904  relexp0  24040  relexpsucr  24041  itg2addnclem  25003  itg2addnc  25005  iscst2  25278  sgplpte21  26235  sgplpte22  26241  isray2  26256  isray  26257  ismtyval  26627  rrnmval  26655  uvcfval  27336  mamufval  27546  mamuval  27547  mamufv  27548  sprmpt2  28207  wlks  28328  trls  28335  pths  28352  spths  28353
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pr 4230
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-sbc 3005  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-opab 4094  df-id 4325  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-iota 5235  df-fun 5273  df-fv 5279  df-ov 5877  df-oprab 5878  df-mpt2 5879
  Copyright terms: Public domain W3C validator