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

Theorem oveqd 6101
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 6090 . 2  |-  ( A  =  B  ->  ( C A D )  =  ( C B D ) )
31, 2syl 16 1  |-  ( ph  ->  ( C A D )  =  ( C B D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653  (class class class)co 6084
This theorem is referenced by:  oveq123d  6105  csbov12g  6116  ovmpt2dxf  6202  oprssov  6218  ofeq  6310  ruclem1  12835  vdwapval  13346  vdwapid1  13348  vdwmc2  13352  vdwpc  13353  vdwlem5  13358  vdwlem8  13361  vdwlem13  13366  prdsval  13683  prdsdsval2  13711  pwsplusgval  13717  pwsmulrval  13718  pwsvscafval  13721  imasval  13742  iscat  13902  iscatd  13903  catidex  13904  catideu  13905  cidfval  13906  cidval  13907  catidd  13910  iscatd2  13911  catlid  13913  catrid  13914  proplem3  13921  homffval  13922  homfeqd  13926  homfeqval  13928  comfffval  13929  comffval  13930  comfeq  13937  comfeqd  13938  comfeqval  13939  catpropd  13940  oppcval  13944  oppcco  13948  monfval  13963  ismon  13964  oppcmon  13969  oppcepi  13970  sectffval  13981  sectfval  13982  invffval  13988  isoval  13995  issubc  14040  issubc3  14051  isfunc  14066  cofuval  14084  cofuval2  14089  funcres  14098  funcres2b  14099  funcres2  14100  funcres2c  14103  isfull  14112  isfth  14116  fullres2c  14141  natfval  14148  isnat  14149  fucval  14160  fucco  14164  fucpropd  14179  homarcl  14188  coafval  14224  resssetc  14252  resscatc  14265  catciso  14267  xpcval  14279  1stfval  14293  2ndfval  14296  prfval  14301  prfcl  14305  evlfval  14319  curfval  14325  curf1cl  14330  curfcl  14334  uncf1  14338  uncf2  14339  diag12  14346  diag2  14347  curf2ndf  14349  hofval  14354  hof1  14356  hof2fval  14357  hofcl  14361  yon12  14367  yon2  14368  hofpropd  14369  joinval  14450  meetval  14457  islat  14481  isdlat  14624  ismnd  14697  plusffval  14707  grpidval  14712  grpidd  14723  ismndd  14724  issubmnd  14729  submnd0  14730  ismhm  14745  issubm  14753  resmhm  14764  resmhm2  14765  resmhm2b  14766  gsumvalx  14779  gsumpropd  14781  gsumress  14782  isgrp  14821  isgrpd2e  14832  grpidd2  14847  grpinvfval  14848  imasgrp2  14938  imasgrp  14939  subg0  14955  subginv  14956  subgcl  14959  isnsg  14974  isghm  15011  resghm  15027  isga  15073  subgga  15082  gasubg  15084  cntzfval  15124  resscntz  15135  odfval  15176  gexval  15217  lsmfval  15277  lsmvalx  15278  oppglsm  15281  subglsm  15310  pj1fval  15331  efgtval  15360  iscmn  15424  iscmnd  15429  submcmn2  15463  iscyg  15494  isrng  15673  rngidss  15695  prdsmgp  15721  mulgass3  15747  dvdsrval  15755  isirred  15809  isdrngd  15865  isdrngrd  15866  subrg1  15883  subrgmcl  15885  subrgdvds  15887  subrguss  15888  subrginv  15889  subrgdv  15890  subrgunit  15891  subrgugrp  15892  abvfval  15911  isabvd  15913  issrngd  15954  islmod  15959  islmodd  15961  scaffval  15973  lmodpropd  16012  lssset  16015  islssd  16017  prdslmodd  16050  islmhm  16108  reslmhm  16133  reslmhm2  16134  reslmhm2b  16135  islbs  16153  issubgrpd2  16265  rlmvneg  16283  rrgval  16352  isassa  16380  isassad  16387  psrval  16434  resspsradd  16484  resspsrmul  16485  resspsrvsca  16486  mplmon2mul  16566  ply1coe  16689  isphl  16864  ipffval  16884  isphld  16890  ocvfval  16898  isobs  16952  xkocnv  17851  submtmd  18139  prdsdsf  18402  ressprdsds  18406  blfvalps  18418  prdsxmslem2  18564  tmsxpsval  18573  ngpds  18655  subgngp  18681  tngngp  18700  isnlm  18716  lssnlm  18741  isphtpy  19011  isphtpc  19024  pi1cpbl  19074  pi1addf  19077  pi1addval  19078  pi1grplem  19079  clmsub  19110  clmvsass  19117  clmvsdir  19118  iscph  19138  cphdir  19172  cphdi  19173  cph2di  19174  cph2subdi  19177  cphass  19178  tchval  19182  ipcau2  19196  tchcphlem1  19197  tchcphlem2  19198  caufval  19233  dvlip2  19884  evl1expd  19963  q1pval  20081  r1pval  20084  dvntaylp  20292  dchrmul  21037  wlkon  21535  trlon  21545  trlonprop  21547  pthon  21580  pthonprop  21582  spthon  21587  spthonprp  21590  isconngra  21664  isconngra1  21665  grpodivval  21836  gxval  21851  subgoov  21898  isrngo  21971  vcoprne  22063  dipfval  22203  ipval  22204  sspgval  22233  sspsval  22235  lnoval  22258  ajfval  22315  dipdir  22348  dipass  22351  htth  22426  rdivmuldivd  24232  isofld  24240  subofld  24250  inftmrel  24255  isinftm  24256  metidval  24290  pstmval  24295  pstmfval  24296  zlm0  24351  zlm1  24352  sitmval  24666  istotbnd  26492  isbnd  26503  rrnequiv  26558  rngohomval  26594  idlval  26637  pridlval  26657  frlmplusgval  27220  frlmvscafval  27221  frlmup1  27241  lsslindf  27291  mamufval  27434  matplusg2  27468  matvsca2  27469  mat1  27473  is2wlkonot  28395  is2spthonot  28396  2wlkonot  28397  2spthonot  28398  2wlksot  28399  2spthsot  28400  2wlkonot3v  28407  2spthonot3v  28408  lflset  29931  islfld  29934  ldualvadd  30001  ldualsmul  30007  ldualvs  30009  isopos  30052  cmtfvalN  30082  iscvlat  30195  ishlat1  30224  lineset  30609  psubspset  30615  paddfval  30668  paddval  30669  ltrnfset  30988  trnfsetN  31026  trlfset  31031  tgrpov  31619  erngplus  31674  erngmul  31677  erngplus-rN  31682  erngmul-rN  31685  erngdvlem3  31861  erngdvlem4  31862  erng0g  31865  erngdvlem3-rN  31869  erngdvlem4-rN  31870  dvaplusg  31880  dvamulr  31883  dvavadd  31886  dvavsca  31888  dvalveclem  31897  dvhmulr  31958  dvhfvadd  31963  dvhvadd  31964  dvhopvadd2  31966  dvhvaddcl  31967  dvhvaddcomN  31968  dvhvsca  31973  dvhlveclem  31980  dvh0g  31983  djavalN  32007  diblsmopel  32043  dicvaddcl  32062  cdlemn6  32074  dihffval  32102  dihopelvalcpre  32120  djhval  32270  lcdvaddval  32470  lcdsmul  32474  lcdvsval  32476  lcdlkreq2N  32495  hvmapffval  32630  hvmapfval  32631  hdmap1fval  32669  hgmapffval  32760  hgmapfval  32761  hgmapadd  32769  hlhilipval  32824  hlhilhillem  32835
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rex 2713  df-uni 4018  df-br 4216  df-iota 5421  df-fv 5465  df-ov 6087
  Copyright terms: Public domain W3C validator