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

Theorem ovmpt2d 6217
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 2442 . 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 6216 1  |-  ( ph  ->  ( A F B )  =  S )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1364    e. wcel 1761  (class class class)co 6090    e. cmpt2 6092
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pr 4528
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2263  df-mo 2264  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-sbc 3184  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-br 4290  df-opab 4348  df-id 4632  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-iota 5378  df-fun 5417  df-fv 5423  df-ov 6093  df-oprab 6094  df-mpt2 6095
This theorem is referenced by:  ovmpt2ga  6219  suppval  6691  sprmpt2d  6741  erov  7193  cnfcomlem  7928  cnfcomlemOLD  7936  swrdval  12309  splval  12389  0csh0  12426  ramval  14065  prdsval  14389  prdsplusgval  14407  prdsmulrval  14409  prdsdsval  14412  prdsvscaval  14413  imasval  14445  imasdsval  14449  divsval  14476  homfval  14627  comffval  14634  comfval  14635  oppccofval  14651  ismon  14668  sectfval  14686  invfval  14693  cofuval  14788  cofu2nd  14791  resfval  14798  isnat  14853  fucval  14864  fucco  14868  setchom  14944  setcco  14947  catchom  14963  catcco  14965  xpcval  14983  xpcid  14995  1stf2  14999  2ndf2  15002  prfval  15005  prf2fval  15007  evlfval  15023  evlf2  15024  evlf2val  15025  evlf1  15026  curfval  15029  uncfval  15040  diagval  15046  hof2fval  15061  hof2val  15062  yonedalem4a  15081  gsumvalx  15497  pj1fval  16184  psrval  17419  frlmphl  18106  uvcfval  18109  mamufval  18183  mamuval  18184  mamufv  18185  mat1ov  18235  mvmulfval  18253  mvmulval  18254  1mavmul  18259  maducoeval  18345  symgmatr01  18360  gsummatr01lem3  18363  gsummatr01lem4  18364  gsummatr01  18365  cnfval  18737  cnpfval  18738  fmval  19416  fmf  19418  fcfval  19506  tsmsval2  19600  blvalps  19860  blval  19861  ishtpy  20444  isphtpy  20453  rrxnm  20795  rrxmval  20804  limcfval  21247  q1pval  21568  r1pval  21571  ttgitvval  23047  ebtwntg  23147  ecgrtg  23148  wlks  23344  trls  23354  pths  23384  spths  23385  vdgrfval  23484  iseupa  23505  ofoprabco  25901  ofcfval  26460  sitmfval  26649  sseqval  26685  sseqf  26689  sseqp1  26692  cndprobval  26730  orvcval  26754  relexp0  27244  relexpsucr  27245  ismtyval  28608  rrnmval  28636  fmuldfeqlem1  29672  wwlk  30224  wwlkn  30225  clwlk  30327  clwwlk  30338  clwwlkn  30339  clwwlknprop  30344  dmatmulcl  30745  scmatmulcl  30752  lmod1lem1  30853  lmod1lem2  30854  lmod1lem3  30855  lmod1lem4  30856  lmod1lem5  30857
  Copyright terms: Public domain W3C validator