Theorem opreq2d 4034

Description: Equality deduction for operation value.

Hypothesis

Ref	Expression
opreq1d.1	⊢ (φ → A = B)

Assertion

Ref	Expression
opreq2d	⊢ (φ → (CFA) = (CFB))

Proof of Theorem opreq2d

Step	Hyp	Ref	Expression
1		opreq1d.1	. 2 ⊢ (φ → A = B)
2		opreq2 4027	. 2 ⊢ (A = B → (CFA) = (CFB))
3	1, 2	syl 10	1 ⊢ (φ → (CFA) = (CFB))

Syntax hints:   → wi 3   = wceq 992  (class class class)co 4021

This theorem is referenced by:  opreq12d 4036  csbopr1g 4046  caoprass 4115  caoprdistr 4120  onopriun 4211  oaass 4331  odi 4346  omass 4347  oeoalem 4359  oeoa 4360  oeoelem 4361  oeoe 4362  nnmsucr 4380  ecoprass 4461  ecoprdi 4462  addasspi 5177  mulasspi 5179  distrpi 5180  addclprlem2 5273  mulclprlem 5275  distrlem4pr 5284  1idpr 5287  prlem934a 5291  prlem936a 5307  prlem936 5309  mulcmpblnrlem 5336  ssgt0sr 5371  supsrlem4 5382  supsr 5385  mulcnsr 5408  ax1id 5436  axcnre 5440  add23 5491  add42 5493  cnegex 5502  negsub 5536  addsubass 5537  subneg 5548  pncan 5551  mul23 5573  muladd 5575  subdi 5581  mul2neg 5608  negdi 5609  negsubdi 5611  submul2 5614  subsub2 5615  subsub4 5618  sub23 5619  nnncan 5620  nppcan2 5624  addsub4 5627  sub4 5630  mulsub 5631  pnncan 5634  divreczi 5884  divrec 5885  divass 5887  divdir 5896  divsubdir 5914  recrec 5915  divmul24 5922  divadddiv 5923  divdivdiv 5924  divcan6 5930  divdiv1 5934  divdiv2 5935  conjmul 5937  nnmulcl 6086  flhalf 6446  quoremz 6451  quoremnn0 6453  modval 6460  modfrac 6464  flmod 6465  intfrac 6466  flmulnn0 6467  flmulnn0OLD 6468  modmulnn 6469  modid 6471  modcyc 6475  modcyc2 6476  modmul1 6478  moddi 6479  modsubdir 6480  icoshftf1olem 6537  seq1val 6677  seq1suclem 6681  seq1m1 6684  ser1p1i 6701  shftcan1 6719  seq1shftid 6721  seq0fval 6730  seqzfval 6732  seqzp1 6743  seqzm1 6744  seq0p1 6746  seqzval2 6748  ser0p1i 6762  expval 6765  expp1 6769  expm1t 6778  exprec 6789  exprecOLD 6790  expadd 6791  expmul 6792  expsub 6793  expsubOLD 6794  expm1 6795  expdiv 6796  expordi 6797  subsq2 6840  binom2 6847  bernneq 6849  bernneqOLD 6850  digit2 6855  digit1 6856  discrlem2 6858  discrlem3 6859  discrlem 6860  nn0opthi 6867  sqrmuli 6906  sqr2irrlem2 6926  sqr2irrlem3 6927  sqr2irrlem5 6929  crui 6938  cru 6939  crreczi 6942  creur 6943  creui 6944  replim 6962  cjval 6964  imre 6974  reim0b 6976  rereb 6977  mulre 6978  readd 7006  resub 7007  imadd 7009  imsub 7010  cjadd 7013  cjmul 7014  addcj 7016  cjsub 7017  recj 7019  cj11OLD 7032  absneg 7034  abscj 7036  abs00i 7044  sqabsadd 7050  sqabssub 7051  absmul 7060  absdiv 7062  absre 7068  absresq 7069  recvalzi 7090  cjdivi 7091  cjdiv 7092  absmax 7100  abstri 7101  recan 7108  abslem2 7112  cau2i 7116  ser1absdiflem 7132  facp1 7139  facnn2 7142  faclbnd 7148  faclbnd4lem1 7151  faclbnd4lem2 7152  faclbnd4lem3 7153  faclbnd4lem4 7154  faclbnd6 7157  bcval 7161  bccmpl 7165  bcn0 7166  bcnn 7167  bcnp11 7168  bcnp1n 7169  bcpasc2 7171  bcpasci 7172  bcpasc 7173  sumeq2 7188  fsump1slem 7215  fsum1ps 7221  fsum3 7227  fsum4 7228  fsumrev 7232  fsummulc1 7236  fsumconst 7241  fsumabs 7246  ser1ser0i 7251  serz1p 7255  serzmulc1 7260  serzmulci 7261  serzrelem 7264  binomlem1 7269  binomlem2 7270  binomlem3 7271  binomlem4 7272  binomlem5 7273  binomlem6 7274  binomi 7275  binom1pi 7276  bcxmas 7279  climaddc1 7321  climsub 7333  caucvgi 7366  caucvg3ai 7367  caucvg3lem 7369  caucvg3i 7370  caucvg3 7371  serzf0i 7372  ser1consti 7374  ser1cmp2i 7380  cvgcmp2lem 7383  cvgcmp2i 7384  cvgcmp2ci 7387  cvgcmp3cei 7391  cvgcmp3cetlem1 7392  cvgcmp3cetlem2 7393  isummulc1 7416  isummulc1iALT 7417  isummulc1ai 7418  infcvglem2 7426  infcvgi 7428  arisumi 7430  geoseri 7439  geolimilem 7440  geolimi 7441  geolim 7442  geolim1 7444  georeclim 7445  geoisumr 7448  geoisum1c 7450  0.999... 7451  cvgratlem1ALT 7452  cvgratlem3ALT 7454  cvgratlem1 7455  cvgratlem3 7457  cvgratlem4 7458  cvgratlem5 7459  fsum0diaglem2 7462  fsum0diag 7463  fsum0diag2 7464  fsum0diag4 7466  efcltlem1 7509  efcltlem2 7510  efseq1ex 7511  ef0lem 7515  erelem2 7525  erelem3 7526  ege2lem2 7533  ege2le3lem2 7534  efaddlem6 7548  efaddlem17 7559  efadd 7572  efsub 7576  efexp 7577  eftlex 7583  ef1tllem 7586  ef01tllem1 7588  ef01tllem2 7589  ef01tllem2OLD 7590  eirrlem2 7595  eirrlem5 7598  eflegeo 7624  efcnlem4 7630  resinval 7641  recosval 7642  efi4p 7643  efival 7655  efmival 7656  efeul 7657  sinadd 7661  cosadd 7662  sinsub 7663  cossub 7664  sincossq 7669  sin2t 7670  cos2t 7671  cos2tsin 7672  sin01bndlem3 7678  cos01bndlem3 7680  absefib 7693  efieq1re 7694  demoivre 7695  acdc3lem 7697  acdc2lem2 7701  acdc2 7702  acdc5lem2 7704  acdc5 7705  acdclem 7706  ruclem4 7725  ruclem32 7753  cnfval 7966  cnpfval 7967  mettri2 8023  mettri4 8024  metsym 8026  mettri3 8028  metxpdval 8039  metxplem4 8043  metxp 8044  tgioolem 8125  iscau3 8149  iscau4 8151  opr1cn 8189  bcthlem1 8210  bcthlem17 8226  bcthlem20 8229  isgrp 8254  grpass 8260  grpidinvlem2 8262  grpsn 8273  grpinvid2 8290  isgrp2i 8293  grpasscan2 8295  grpinvop 8298  grpdivfval 8299  grpdivval 8300  grpdivinv 8301  grpdivdiv 8305  grpmuldivass 8306  grppncan 8308  grpnpcan 8309  grppnpcan2 8310  gxval 8314  gxnn0neg 8319  gxnn0suc 8320  gxneg 8322  gxcom 8325  gxsuc 8328  gxnn0add 8330  gxadd 8331  gxsub 8332  gxnn0mul 8333  gxmul 8334  gxmodid 8335  abl23 8345  abldivdiv4 8350  abldiv23 8351  ablnnncan 8352  issubgi 8364  ablmul 8372  ghgrpilem1 8374  ghgrpilem4 8377  isring 8382  ringi 8383  ringdi 8388  ringdir 8389  ringass 8390  ringsn 8405  vci 8414  vcdi 8418  vcdir 8419  vcass 8420  vcsubdir 8422  vcz 8436  vcm 8437  vcrinv 8438  vcnegsubdi2 8441  vcsub4 8442  isvclem 8443  vcoprne 8445  isnvlem 8476  nvi 8480  nvmval 8510  nvmfval 8511  nvmdi 8517  nvrinv 8520  nvsubadd 8522  nvaddsub4 8528  nvnncan 8530  nvs 8537  nvdif 8540  nvpi 8541  nvtri 8545  nvmtri 8546  nvabs 8548  nvge0 8549  cnnvm 8560  nvnd 8566  imsmetlem 8570  ipfval 8606  ipval 8607  ipval2lem3 8609  ipval2 8611  4ipval2 8612  ipval3 8613  ipval2lem6 8615  4ipval3 8616  ipid 8617  ipcj 8621  ipipcj 8622  ip0r 8624  ip1cnilem4 8630  ip1cnilem6 8632  sspmval 8646  sspival 8651  lnoval 8667  islno 8668  lnolin 8669  lno0 8671  lnocoi 8672  lnoadd 8673  0lno 8705  nmlnoubi 8711  nmblolbii 8714  blometi 8718  blocnilem 8719  isphg 8732  cnph 8734  isph 8737  phpar2 8738  phpar 8739  ipdiri 8745  ipasslem1 8746  ipasslem2 8747  ipasslem5 8750  ipasslem11 8756  ipassi 8757  ipass 8761  ipassr 8762  ipsubdir 8764  pythi 8766  siilem1 8767  siilem2 8768  siii 8769  sii 8770  sspph 8771  ipblnfi 8772  ajmoi 8775  ubthlem8 8794  ubthlem10 8796  minveclem6 8810  minveclem8 8812  minveclem19 8823  minveclem21 8825  minveclem23 8827  minveclem30 8834  minveclem36 8840  minveceu 8843  htthlem2 8883  htthlem3 8884  laspwcl 8930  lanfwcl 8931  sinper 8957  cosper 8958  efimpi 8965  abssinper 8980  sineq0 8983  sineq0OLD 8984  efifolem2 8995  efifolem3 8996  efifolem6 8999  shftefif1olem 9013  effoi 9017  efper 9019  hvsubval 9161  hvaddsubval 9177  hvadd23 9178  hvsub4 9181  hvaddsub12 9182  hvpncan 9183  hvaddsubass 9185  hvsubdistr1 9191  hvsubdistr2 9192  hvsubsub4 9202  hvnegdi 9209  hvaddsub4 9221  his5 9229  his2sub 9234  normlem6 9257  normlem9at 9263  norm-ii 9281  norm-iii 9283  normpythi 9285  normpyth 9288  norm3dif 9293  norm3adifi 9296  normpar 9298  polid 9302  hhph 9321  bcsiALT 9322  bcs 9324  hcau2 9331  hhssnv 9410  chocunii 9448  occllem2 9450  projlem7 9468  projlem17 9478  projlem20 9481  projlem22 9483  projlem26 9487  pjthlem8 9502  pjthlem9 9503  omlsilem 9520  pjchi 9541  chdmm1 9724  chdmm3 9726  chdmm4 9727  chjass 9732  chj4 9734  ledi 9739  spanun 9744  h1de2bi 9753  pjspansn 9776  spanunsni 9778  hosmval 9787  hommval 9788  hodmval 9789  hfsmval 9790  hfmmval 9791  homval 9794  hfmval 9798  cmcmlem 9810  pjoml2 9830  spansnj 9870  spansncv 9876  5oalem1 9877  5oalem2 9878  5oalem3 9879  5oalem5 9881  3oalem2 9886  pjcji 9907  pjadji 9908  pjaddi 9909  pjsubi 9911  pjmuli 9912  pjcjt2 9915  pjopyth 9943  hoaddassi 9982  hoaddass 9988  hoadd23 9989  hocsubdir 9991  hoaddid1i 9992  honegsubi 10002  ho0sub 10003  honegsub 10005  homco1 10007  homulass 10008  hoadddi 10009  hosubneg 10013  hosubdi 10014  honegsubdi 10016  hosubsub2 10018  hosub4 10019  hoaddsubass 10021  hosubsub4 10024  adjsym 10039  eigorth 10044  ellnop 10064  elhmop 10080  ellnfn 10090  adjval 10094  cnopc 10117  lnopl 10118  unop 10119  unopadj 10123  unoplin 10124  hmop 10126  cnfnc 10134  lnfnl 10135  adj1 10137  adjeq 10139  hmoplin 10146  bramul 10150  brafnmul 10155  kbpj 10160  lnopmul 10170  lnopaddmuli 10176  lnopsubmuli 10178  homco2 10180  0hmop 10186  0lnfn 10188  hoddi 10194  adj0 10198  lnopmi 10204  lnophsi 10205  lnopcoi 10207  lnopeq0lem2 10210  lnopeq0i 10211  lnopunii 10216  lnophmi 10222  lnophm 10223  hmops 10224  hmopm 10225  hmopco 10227  nmbdoplbi 10228  nmcoplbi 10237  lnopconi 10242  lnfnaddmuli 10253  lnfnsubi 10254  lnfnmul 10256  nmbdfnlbi 10257  nmcfnlbi 10266  lnfnconi 10269  nlelshi 10272  cnlnadjlem2 10280  cnlnadjlem5 10283  cnlnadjlem6 10284  cnlnadjlem9 10287  cnlnssadj 10292  adjlnop 10298  adjmul 10304  adjadd 10305  nmopcoi 10307  adjcoi 10312  unierri 10316  branmfn 10317  branmfnOLD 10318  cnvbraval 10323  cnvbramul 10328  kbass6 10334  leopnmid 10351  hmopidmchi 10359  hmopidmpji 10360  pjadjcoi 10369  pjss2coi 10372  pjclem4 10408  pjadj2coi 10413  pj3si 10416  pj3cor1i 10418  hstel2 10427  hst1h 10435  hstle 10438  hstoh 10440  stj 10443  st0 10457  stcltrlem1 10484  mdbr 10502  dmdmd 10508  ssmd1 10519  ssmd2 10520  mdslmd1lem2 10534  mdslmd3i 10540  cvexchlem 10576  atoml2i 10592  irredlem3 10601  atcvat3i 10605  atabsi 10610  sumdmdlem2 10628  cdj1i 10642  cdj3lem1 10643  cdj3lem2b 10646  cdj3lem3b 10649  cdj3i 10650  ghomgrpilem1 10670  ghomlin 10678  symggrpi 10691  cayleylem2 10695  opreq123d 10777  islatalg 10831  labss1 10837  labss2 10839  isass 10890  smgrpass2 10914  seqzp2 10918  mndass2 10932  zerab2 10958  multinvb 10960  zrdivrng 10969  vri 10981  hmeogrp 11044  mslb1 11152  iscat 11208  cati 11209  1cat 11213  cmpasso 11227  cmpidb 11229  fmufil 11705  filnet 11768  isgalem 11771  ssga 11777  gaass 11781  divexp 11859  fzm1 11867  rddif 11869  sdclem2 11876  sdc 11877  fsumltisumi 11886  fsumlt1 11894  csbrni 11895  trirn 11897  metf1o 11907  mettrifi 11912  mettrifi2 11913  geomcau 11914  caushft 11916  lincmb01cmp 11942  isbnd3 11997  ismtycnv 12005  ismtyhmeolem 12006  ismtyhmeo 12007  ismtybndlem 12008  ismtyres 12010  heiborlem16 12026  heiborlem25 12035  heiborlem26 12036  heiborlem32 12042  heiborlem33 12043  heiborlem35 12045  bfplem5 12058  bfplem6 12059  bfplem7 12060  bfplem8 12061  bfplem9 12062  bfplem11 12064  bfp 12065  recms 12066  rrnval 12069  rrnmval 12070  rrntotbndlem1 12076  rrntotbndlem2 12077  phtpycom 12092  phtpycolem1 12093  phtpycolem2 12094

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-sep 2777  ax-pow 2818  ax-pr 2855

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-v 1858  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-nul 2333  df-pw 2459  df-sn 2470  df-pr 2471  df-op 2474  df-uni 2570  df-br 2693  df-opab 2741  df-xp 3265  df-cnv 3267  df-dm 3269  df-rn 3270  df-res 3271  df-ima 3272  df-fv 3279  df-opr 4023

Copyright terms: Public domain