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

Theorem oveqd 5875
Description: Equality deduction for operation value. (Contributed by NM, 9-Sep-2006.)
Hypothesis
Ref Expression
oveq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
oveqd  |-  ( ph  ->  ( C A D )  =  ( C B D ) )

Proof of Theorem oveqd
StepHypRef Expression
1 oveq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 oveq 5864 . 2  |-  ( A  =  B  ->  ( C A D )  =  ( C B D ) )
31, 2syl 15 1  |-  ( ph  ->  ( C A D )  =  ( C B D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623  (class class class)co 5858
This theorem is referenced by:  oveq123d  5879  csbov12g  5890  ovmpt2dxf  5973  oprssov  5989  ofeq  6080  ruclem1  12509  vdwapval  13020  vdwapid1  13022  vdwmc2  13026  vdwpc  13027  vdwlem5  13032  vdwlem8  13035  vdwlem13  13040  prdsval  13355  prdsdsval2  13383  pwsplusgval  13389  pwsmulrval  13390  pwsvscafval  13393  imasval  13414  iscat  13574  iscatd  13575  catidex  13576  catideu  13577  cidfval  13578  cidval  13579  catidd  13582  iscatd2  13583  catlid  13585  catrid  13586  proplem3  13593  homffval  13594  homfeqd  13598  homfeqval  13600  comfffval  13601  comffval  13602  comfeq  13609  comfeqd  13610  comfeqval  13611  catpropd  13612  oppcval  13616  oppcco  13620  monfval  13635  ismon  13636  oppcmon  13641  oppcepi  13642  sectffval  13653  sectfval  13654  invffval  13660  isoval  13667  issubc  13712  issubc3  13723  fullresc  13725  isfunc  13738  cofuval  13756  cofuval2  13761  funcres  13770  funcres2b  13771  funcres2  13772  funcres2c  13775  isfull  13784  isfth  13788  fullres2c  13813  natfval  13820  isnat  13821  fucval  13832  fucco  13836  fucpropd  13851  homarcl  13860  coafval  13896  resssetc  13924  resscatc  13937  catciso  13939  xpcval  13951  1stfval  13965  2ndfval  13968  prfval  13973  prfcl  13977  evlfval  13991  curfval  13997  curf1  13999  curf1cl  14002  curfcl  14006  uncf1  14010  uncf2  14011  diag12  14018  diag2  14019  curf2ndf  14021  hofval  14026  hof1  14028  hof2fval  14029  hofcl  14033  yon12  14039  yon2  14040  hofpropd  14041  joinval  14122  meetval  14129  islat  14153  isdlat  14296  ismnd  14369  plusffval  14379  grpidval  14384  grpidd  14395  ismndd  14396  issubmnd  14401  submnd0  14402  ismhm  14417  issubm  14425  resmhm  14436  resmhm2  14437  resmhm2b  14438  gsumvalx  14451  gsumpropd  14453  gsumress  14454  isgrp  14493  isgrpd2e  14504  grpidd2  14519  grpinvfval  14520  imasgrp2  14610  imasgrp  14611  subg0  14627  subginv  14628  subgcl  14631  isnsg  14646  isghm  14683  resghm  14699  isga  14745  subgga  14754  gasubg  14756  cntzfval  14796  resscntz  14807  odfval  14848  gexval  14889  sylow2blem2  14932  lsmfval  14949  lsmvalx  14950  oppglsm  14953  subglsm  14982  pj1fval  15003  efgtval  15032  iscmn  15096  iscmnd  15101  submcmn2  15135  iscyg  15166  isrng  15345  rngidss  15367  isrngd  15375  prdsmgp  15393  mulgass3  15419  dvdsrval  15427  isirred  15481  isdrngd  15537  isdrngrd  15538  subrg1  15555  subrgmcl  15557  subrgdvds  15559  subrguss  15560  subrginv  15561  subrgdv  15562  subrgunit  15563  subrgugrp  15564  abvfval  15583  isabvd  15585  issrngd  15626  islmod  15631  islmodd  15633  scaffval  15645  lmodpropd  15688  lssset  15691  islssd  15693  prdslmodd  15726  islmhm  15784  reslmhm  15809  reslmhm2  15810  reslmhm2b  15811  islbs  15829  issubgrpd2  15941  rlmvneg  15959  rrgval  16028  isdomn  16035  isassa  16056  isassad  16063  psrval  16110  resspsradd  16160  resspsrmul  16161  resspsrvsca  16162  mplmon2mul  16242  ply1coe  16368  isphl  16532  ipffval  16552  isphld  16558  ocvfval  16566  isobs  16620  xkocnv  17505  submtmd  17787  prdsdsf  17931  ressprdsds  17935  blfval  17947  prdsxmslem2  18075  tmsxpsval  18084  ngpds  18125  subgngp  18151  tngngp  18170  isnlm  18186  lssnlm  18211  isphtpy  18479  isphtpc  18492  pi1cpbl  18542  pi1addf  18545  pi1addval  18546  pi1grplem  18547  clmsub  18578  clmvsass  18585  clmvsdir  18586  iscph  18606  cphdir  18640  cphdi  18641  cph2di  18642  cph2subdi  18645  cphass  18646  tchval  18650  ipcau2  18664  tchcphlem1  18665  tchcphlem2  18666  caufval  18701  dvlip2  19342  evl1expd  19421  q1pval  19539  r1pval  19542  dvntaylp  19750  dchrmul  20487  grpodivval  20910  gxval  20925  subgoov  20972  isrngo  21045  vcoprne  21135  dipfval  21275  ipval  21276  sspgval  21305  sspsval  21307  lnoval  21330  ajfval  21387  dipdir  21420  dipass  21423  htth  21498  oprssopvg  25034  iscst1  25174  idlvalNEW  25445  isaddrv  25646  cnegvex2b  25662  rnegvex2b  25663  issubcv  25670  ismulcv  25681  isdivcv2  25693  isder  25707  ismona  25809  isepia  25819  isiso  25825  cinvlem1  25828  isfuna  25834  islimcat  25876  cmp2morp  25958  lineval222  26079  lineval3a  26083  sgplpte21  26132  sgplpte22  26138  isray2  26153  isray  26154  isside0  26164  istotbnd  26493  isbnd  26504  rrnequiv  26559  rngohomval  26595  idlval  26638  pridlval  26658  frlmplusgval  27229  frlmvscafval  27230  frlmup1  27250  lsslindf  27300  mamufval  27443  matplusg2  27477  matvsca2  27478  mat1  27482  mendval  27491  lflset  29249  islfld  29252  ldualvadd  29319  ldualsmul  29325  ldualvs  29327  isopos  29370  cmtfvalN  29400  iscvlat  29513  ishlat1  29542  lineset  29927  psubspset  29933  paddfval  29986  paddval  29987  ltrnfset  30306  trnfsetN  30344  trlfset  30349  tgrpov  30937  erngplus  30992  erngmul  30995  erngplus-rN  31000  erngmul-rN  31003  erngdvlem3  31179  erngdvlem4  31180  erng0g  31183  erngdvlem3-rN  31187  erngdvlem4-rN  31188  dvaplusg  31198  dvamulr  31201  dvavadd  31204  dvavsca  31206  dvalveclem  31215  dvhmulr  31276  dvhfvadd  31281  dvhvadd  31282  dvhopvadd2  31284  dvhvaddcl  31285  dvhvaddcomN  31286  dvhvsca  31291  dvhlveclem  31298  dvh0g  31301  djavalN  31325  diblsmopel  31361  dicvaddcl  31380  cdlemn6  31392  dihffval  31420  dihopelvalcpre  31438  djhval  31588  lcdvaddval  31788  lcdsmul  31792  lcdvsval  31794  lcdlkreq2N  31813  hvmapffval  31948  hvmapfval  31949  hdmap1fval  31987  hgmapffval  32078  hgmapfval  32079  hgmapadd  32087  hlhilipval  32142  hlhilhillem  32153
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861
  Copyright terms: Public domain W3C validator