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

Theorem ovmpt2d 6168
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 2413 . 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 6167 1  |-  ( ph  ->  ( A F B )  =  S )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649    e. wcel 1721  (class class class)co 6048    e. cmpt2 6050
This theorem is referenced by:  ovmpt2ga  6170  sprmpt2  6443  erov  6968  cnfcomlem  7620  swrdval  11727  splval  11743  ramval  13339  prdsval  13641  prdsplusgval  13658  prdsmulrval  13660  prdsdsval  13663  prdsvscaval  13664  imasval  13700  imasdsval  13704  divsval  13730  homfval  13881  comffval  13888  comfval  13889  oppccofval  13905  ismon  13922  sectfval  13940  invfval  13947  cofuval  14042  cofu2nd  14045  resfval  14052  isnat  14107  fucval  14118  fucco  14122  setchom  14198  setcco  14201  catchom  14217  catcco  14219  xpcval  14237  xpcid  14249  1stf2  14253  2ndf2  14256  prfval  14259  prf2fval  14261  evlfval  14277  evlf2  14278  evlf2val  14279  evlf1  14280  curfval  14283  uncfval  14294  diagval  14300  hof2fval  14315  hof2val  14316  yonedalem4a  14335  gsumvalx  14737  pj1fval  15289  psrval  16392  cnfval  17259  cnpfval  17260  fmval  17936  fmf  17938  fcfval  18026  tsmsval2  18120  blvalps  18376  blval  18377  ishtpy  18958  isphtpy  18967  limcfval  19720  q1pval  20037  r1pval  20040  wlks  21487  trls  21497  pths  21527  spths  21528  vdgrfval  21627  iseupa  21648  ofoprabco  24040  ofcfval  24442  sitmfval  24623  cndprobval  24652  orvcval  24676  relexp0  25090  relexpsucr  25091  ismtyval  26407  rrnmval  26435  uvcfval  27109  mamufval  27319  mamuval  27320  mamufv  27321  fmuldfeqlem1  27587
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 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-sep 4298  ax-nul 4306  ax-pr 4371
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 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-ral 2679  df-rex 2680  df-rab 2683  df-v 2926  df-sbc 3130  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597  df-if 3708  df-sn 3788  df-pr 3789  df-op 3791  df-uni 3984  df-br 4181  df-opab 4235  df-id 4466  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-iota 5385  df-fun 5423  df-fv 5429  df-ov 6051  df-oprab 6052  df-mpt2 6053
  Copyright terms: Public domain W3C validator