Theorem ovmpt2d 6788

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

Step	Hyp	Ref	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 2623	. 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 )
7	1, 2, 3, 4, 5, 6	ovmpt2dx 6787	1 |- ( ph -> ( A F B ) = S )

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483   e. wcel 1990  (class class class)co 6650   |-> cmpt2 6652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-iota 5851  df-fun 5890  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655

This theorem is referenced by:  ovmpt2ga  6790  el2mpt2csbcl  7250  suppval  7297  sprmpt2d  7350  mpt2curryd  7395  erov  7844  cnfcomlem  8596  swrdval  13417  splval  13502  0csh0  13539  relexp0g  13762  relexpsucnnr  13765  relexp1g  13766  ramval  15712  prdsval  16115  prdsplusgval  16133  prdsmulrval  16135  prdsdsval  16138  prdsvscaval  16139  imasval  16171  imasdsval  16175  qusval  16202  homfval  16352  comffval  16359  comfval  16360  oppccofval  16376  ismon  16393  sectfval  16411  invfval  16419  cofuval  16542  cofu2nd  16545  resfval  16552  isnat  16607  fucval  16618  fucco  16622  setchom  16730  setcco  16733  catchom  16749  catcco  16751  estrchom  16767  estrcco  16770  funcestrcsetclem5  16784  funcsetcestrclem5  16799  xpcval  16817  xpcid  16829  1stf2  16833  2ndf2  16836  prfval  16839  prf2fval  16841  evlfval  16857  evlf2  16858  evlf2val  16859  evlf1  16860  curfval  16863  uncfval  16874  diagval  16880  hof2fval  16895  hof2val  16896  yonedalem4a  16915  gsumvalx  17270  mgm2nsgrplem2  17406  mgm2nsgrplem3  17407  sgrp2nmndlem2  17411  sgrp2nmndlem3  17412  pj1fval  18107  isrim0  18723  rmodislmodlem  18930  rmodislmod  18931  psrval  19362  frlmphl  20120  uvcfval  20123  mamufval  20191  mamuval  20192  mamufv  20193  matinvgcell  20241  mpt2matmul  20252  mat1ov  20254  dmatval  20298  dmatmulcl  20306  scmatval  20310  scmatscmiddistr  20314  scmatscm  20319  mvmulfval  20348  mvmulval  20349  1mavmul  20354  maducoeval  20445  symgmatr01  20460  gsummatr01lem3  20463  gsummatr01lem4  20464  gsummatr01  20465  cpmat  20514  mat2pmatfval  20528  mat2pmatvalel  20530  mat2pmatmul  20536  cpm2mfval  20554  cpm2mvalel  20556  m2cpminvid  20558  m2cpminvid2  20560  decpmatval0  20569  decpmate  20571  decpmataa0  20573  decpmatmul  20577  pmatcollpw1  20581  monmatcollpw  20584  pmatcollpwlem  20585  pmatcollpw  20586  pmatcollpwscmatlem2  20595  pm2mpval  20600  pm2mpf1  20604  mptcoe1matfsupp  20607  mp2pm2mplem3  20613  mp2pm2mplem4  20614  chmatval  20634  chpmatfval  20635  chp0mat  20651  cnfval  21037  cnpfval  21038  fmval  21747  fmf  21749  fcfval  21837  tsmsval2  21933  blvalps  22190  blval  22191  ishtpy  22771  isphtpy  22780  rrxnm  23179  rrxmval  23188  limcfval  23636  q1pval  23913  r1pval  23916  ismidb  25670  ttgitvval  25762  ebtwntg  25862  ecgrtg  25863  ewlksfval  26497  wwlksn  26729  wwlksnon  26738  wspthsnon  26739  iswwlksnon  26740  iswspthsnon  26741  clwwlksn  26881  ofoprabco  29464  smatfval  29861  lmatfval  29880  mdetpmtr1  29889  ofcfval  30160  sitmfval  30412  sseqval  30450  sseqf  30454  sseqp1  30457  cndprobval  30495  orvcval  30519  reprval  30688  mclsval  31460  fwddifnval  32270  finxpreclem1  33226  finxpreclem3  33230  ismtyval  33599  rrnmval  33627  rfovd  38295  fsovd  38302  fsovrfovd  38303  bccval  38537  fmuldfeqlem1  39814  rrndistlt  40510  hoidmvval  40791  hspval  40823  hoiqssbllem2  40837  smflimlem3  40981  pfxval  41383  copissgrp  41808  copisnmnd  41809  intopval  41838  rnghmval  41891  isrngisom  41896  rhmval  41919  cznrng  41955  rnghmsscmap2  41973  rnghmsscmap  41974  rngchomALTV  41985  rngccoALTV  41988  funcrngcsetc  41998  funcrngcsetcALT  41999  rhmsscmap2  42019  rhmsscmap  42020  funcringcsetc  42035  funcringcsetcALTV2lem5  42040  ringchomALTV  42048  ringccoALTV  42051  funcringcsetclem5ALTV  42063  srhmsubclem3  42075  srhmsubc  42076  fldhmsubc  42084  srhmsubcALTVlem2  42093  srhmsubcALTV  42094  fldhmsubcALTV  42102  lmod1lem1  42276  lmod1lem2  42277  lmod1lem3  42278  lmod1lem4  42279  lmod1lem5  42280  offval0  42299  fdivval  42333  digval  42392