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

Theorem ovmpt2d 6218
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 2444 . 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 6217 1  |-  ( ph  ->  ( A F B )  =  S )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1369    e. wcel 1756  (class class class)co 6091    e. cmpt2 6093
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4413  ax-nul 4421  ax-pr 4531
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-sbc 3187  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-br 4293  df-opab 4351  df-id 4636  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-iota 5381  df-fun 5420  df-fv 5426  df-ov 6094  df-oprab 6095  df-mpt2 6096
This theorem is referenced by:  ovmpt2ga  6220  suppval  6692  sprmpt2d  6742  mpt2curryd  6788  erov  7197  cnfcomlem  7932  cnfcomlemOLD  7940  swrdval  12313  splval  12393  0csh0  12430  ramval  14069  prdsval  14393  prdsplusgval  14411  prdsmulrval  14413  prdsdsval  14416  prdsvscaval  14417  imasval  14449  imasdsval  14453  divsval  14480  homfval  14631  comffval  14638  comfval  14639  oppccofval  14655  ismon  14672  sectfval  14690  invfval  14697  cofuval  14792  cofu2nd  14795  resfval  14802  isnat  14857  fucval  14868  fucco  14872  setchom  14948  setcco  14951  catchom  14967  catcco  14969  xpcval  14987  xpcid  14999  1stf2  15003  2ndf2  15006  prfval  15009  prf2fval  15011  evlfval  15027  evlf2  15028  evlf2val  15029  evlf1  15030  curfval  15033  uncfval  15044  diagval  15050  hof2fval  15065  hof2val  15066  yonedalem4a  15085  gsumvalx  15502  pj1fval  16191  isrim0  16813  psrval  17429  frlmphl  18206  uvcfval  18209  mamufval  18283  mamuval  18284  mamufv  18285  mat1ov  18335  mvmulfval  18353  mvmulval  18354  1mavmul  18359  maducoeval  18445  symgmatr01  18460  gsummatr01lem3  18463  gsummatr01lem4  18464  gsummatr01  18465  cnfval  18837  cnpfval  18838  fmval  19516  fmf  19518  fcfval  19606  tsmsval2  19700  blvalps  19960  blval  19961  ishtpy  20544  isphtpy  20553  rrxnm  20895  rrxmval  20904  limcfval  21347  q1pval  21625  r1pval  21628  ttgitvval  23128  ebtwntg  23228  ecgrtg  23229  wlks  23425  trls  23435  pths  23465  spths  23466  vdgrfval  23565  iseupa  23586  ofoprabco  25982  ofcfval  26540  sitmfval  26735  sseqval  26771  sseqf  26775  sseqp1  26778  cndprobval  26816  orvcval  26840  relexp0  27331  relexpsucr  27332  ismtyval  28699  rrnmval  28727  fmuldfeqlem1  29763  wwlk  30315  wwlkn  30316  clwlk  30418  clwwlk  30429  clwwlkn  30430  clwwlknprop  30435  dmatmulcl  30879  scmatmulcl  30886  mptcoe1matfsupp  30891  pmatcollpw1lem1  30896  pmatcollpw1lem3  30898  pmatcollpw1dst  30901  pmatcollpw1  30904  pmattomply1lem  30908  mp2pm2mplem3  30918  mp2pm2mplem4  30919  pmattomply1f1  30922  lmod1lem1  31029  lmod1lem2  31030  lmod1lem3  31031  lmod1lem4  31032  lmod1lem5  31033
  Copyright terms: Public domain W3C validator