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

Theorem ovmpt2d 6160
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 2405 . 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 6159 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 6040    e. cmpt2 6042
This theorem is referenced by:  ovmpt2ga  6162  sprmpt2  6435  erov  6960  cnfcomlem  7612  swrdval  11719  splval  11735  ramval  13331  prdsval  13633  prdsplusgval  13650  prdsmulrval  13652  prdsdsval  13655  prdsvscaval  13656  imasval  13692  imasdsval  13696  divsval  13722  homfval  13873  comffval  13880  comfval  13881  oppccofval  13897  ismon  13914  sectfval  13932  invfval  13939  cofuval  14034  cofu2nd  14037  resfval  14044  isnat  14099  fucval  14110  fucco  14114  setchom  14190  setcco  14193  catchom  14209  catcco  14211  xpcval  14229  xpcid  14241  1stf2  14245  2ndf2  14248  prfval  14251  prf2fval  14253  evlfval  14269  evlf2  14270  evlf2val  14271  evlf1  14272  curfval  14275  uncfval  14286  diagval  14292  hof2fval  14307  hof2val  14308  yonedalem4a  14327  gsumvalx  14729  pj1fval  15281  psrval  16384  cnfval  17251  cnpfval  17252  fmval  17928  fmf  17930  fcfval  18018  tsmsval2  18112  blvalps  18368  blval  18369  ishtpy  18950  isphtpy  18959  limcfval  19712  q1pval  20029  r1pval  20032  wlks  21479  trls  21489  pths  21519  spths  21520  vdgrfval  21619  iseupa  21640  ofoprabco  24032  ofcfval  24434  sitmfval  24615  cndprobval  24644  orvcval  24668  relexp0  25082  relexpsucr  25083  ismtyval  26399  rrnmval  26427  uvcfval  27101  mamufval  27311  mamuval  27312  mamufv  27313  fmuldfeqlem1  27579
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 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363
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 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-iota 5377  df-fun 5415  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045
  Copyright terms: Public domain W3C validator