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

Theorem ovmpt2d 6414
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 2468 . 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 6413 1  |-  ( ph  ->  ( A F B )  =  S )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1379    e. wcel 1767  (class class class)co 6284    |-> cmpt2 6286
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-iota 5551  df-fun 5590  df-fv 5596  df-ov 6287  df-oprab 6288  df-mpt2 6289
This theorem is referenced by:  ovmpt2ga  6416  suppval  6903  sprmpt2d  6952  mpt2curryd  6998  erov  7408  cnfcomlem  8143  cnfcomlemOLD  8151  swrdval  12607  splval  12690  0csh0  12727  ramval  14385  prdsval  14710  prdsplusgval  14728  prdsmulrval  14730  prdsdsval  14733  prdsvscaval  14734  imasval  14766  imasdsval  14770  divsval  14797  homfval  14948  comffval  14955  comfval  14956  oppccofval  14972  ismon  14989  sectfval  15007  invfval  15014  cofuval  15109  cofu2nd  15112  resfval  15119  isnat  15174  fucval  15185  fucco  15189  setchom  15265  setcco  15268  catchom  15284  catcco  15286  xpcval  15304  xpcid  15316  1stf2  15320  2ndf2  15323  prfval  15326  prf2fval  15328  evlfval  15344  evlf2  15345  evlf2val  15346  evlf1  15347  curfval  15350  uncfval  15361  diagval  15367  hof2fval  15382  hof2val  15383  yonedalem4a  15402  gsumvalx  15824  pj1fval  16518  isrim0  17173  psrval  17810  frlmphl  18607  uvcfval  18610  mamufval  18682  mamuval  18683  mamufv  18684  matinvgcell  18732  mpt2matmul  18743  mat1ov  18745  dmatval  18789  dmatmulcl  18797  scmatval  18801  scmatscmiddistr  18805  scmatscm  18810  mvmulfval  18839  mvmulval  18840  1mavmul  18845  maducoeval  18936  symgmatr01  18951  gsummatr01lem3  18954  gsummatr01lem4  18955  gsummatr01  18956  cpmat  19005  mat2pmatfval  19019  mat2pmatvalel  19021  mat2pmatmul  19027  cpm2mfval  19045  cpm2mvalel  19047  m2cpminvid  19049  m2cpminvid2  19051  decpmatval0  19060  decpmate  19062  decpmataa0  19064  decpmatmul  19068  pmatcollpw1  19072  monmatcollpw  19075  pmatcollpwlem  19076  pmatcollpw  19077  pmatcollpwscmatlem2  19086  pm2mpval  19091  pm2mpf1  19095  mptcoe1matfsupp  19098  mp2pm2mplem3  19104  mp2pm2mplem4  19105  chmatval  19125  chpmatfval  19126  chp0mat  19142  cnfval  19528  cnpfval  19529  fmval  20207  fmf  20209  fcfval  20297  tsmsval2  20391  blvalps  20651  blval  20652  ishtpy  21235  isphtpy  21244  rrxnm  21586  rrxmval  21595  limcfval  22039  q1pval  22317  r1pval  22320  ismidb  23849  ttgitvval  23889  ebtwntg  23989  ecgrtg  23990  wlks  24223  trls  24242  pths  24272  spths  24273  wwlk  24385  wwlkn  24386  clwlk  24457  clwwlk  24470  clwwlkn  24471  clwwlknprop  24476  vdgrfval  24599  iseupa  24669  ofoprabco  27205  ofcfval  27765  sitmfval  27959  sseqval  27995  sseqf  27999  sseqp1  28002  cndprobval  28040  orvcval  28064  relexp0  28555  relexpsucr  28556  ismtyval  29927  rrnmval  29955  fmuldfeqlem1  31160  intopval  31982  lmod1lem1  32187  lmod1lem2  32188  lmod1lem3  32189  lmod1lem4  32190  lmod1lem5  32191
  Copyright terms: Public domain W3C validator