Theorem opreq2i 3972

Description: Equality inference for operation value.

Hypothesis

Ref	Expression
opreq1i.1	|- A = B

Assertion

Ref	Expression
opreq2i	|- (CFA) = (CFB)

Proof of Theorem opreq2i

Step	Hyp	Ref	Expression
1		opreq1i.1	. 2 |- A = B
2		opreq2 3969	. 2 |- (A = B -> (CFA) = (CFB))
3	1, 2	ax-mp 7	1 |- (CFA) = (CFB)

Syntax hints:   = wceq 956  (class class class)co 3963

This theorem is referenced by:  opreq12i 3973  caopr32 4060  caopr4 4064  caopr42 4066  oa1suc 4164  om1 4176  oe1 4178  oawordeulem 4188  nneob 4255  cdaassen 4930  mapcdaen 4932  addasspq 5063  mulidpq 5069  addclprlem2 5119  prlem934a 5137  prlem936a 5153  mulcmpblnrlem 5182  m1p1sr 5201  m1m1sr 5202  0idsr 5206  1idsr 5207  00sr 5208  pn0sr 5210  recexsrlem 5212  mulgt0sr 5214  sqgt0sr 5215  mappsrpr 5218  supsrlem2 5226  supsrlem5 5229  mulresr 5257  axmulcom 5276  axmulass 5278  axdistr 5279  ax0id 5281  ax1id 5282  axi2m1 5285  axcnre 5286  add42 5343  negidt 5379  negsub 5381  negneg 5390  neg11 5406  mul01 5431  negsubdi 5449  ltsubadd 5594  ltneg 5603  ixi 5681  muleqaddt 5700  divrec 5737  recrec 5769  rec11i 5777  2p2e4 6001  3p2e5 6007  3p3e6 6008  4p2e6 6009  4p3e7 6010  4p4e8 6011  5p2e7 6012  5p3e8 6013  5p4e9 6014  5p5e10 6015  6p2e8 6016  6p3e9 6017  6p4e10 6018  7p2e9 6019  7p3e10 6020  8p2e10 6021  3t3e9 6024  8th4div3 6031  halfpm6th 6032  halfpost 6036  nneo 6197  zeot 6199  quoremz 6251  intfrac 6253  intfracOLD 6254  intfracqOLD 6255  shftidt 6355  fzshftralt 6522  seq1seqz 6541  seq0seqz 6542  seq1seq0t 6544  seqzres2 6561  expp1t 6574  sqvalt 6609  sqreci 6619  cu2 6640  binom2 6644  discrlem1 6656  discrlem3 6658  nnesq 6662  nn0opthlem1 6664  sqrlem2 6674  sqrlem11 6683  sqr2irrlem1 6724  i3 6733  i4 6734  crulem 6736  crmul 6740  crrecz 6741  cjcj 6778  recj 6782  imcj 6783  readd 6784  imadd 6785  cjadd 6788  cjmul 6789  ipcn 6790  cjmulrcl 6791  reneg 6794  imneg 6796  cjneg 6797  addcj 6798  cji 6827  absmul 6847  absid 6861  absi 6878  cjdiv 6888  abstri 6891  abslem2i 6908  faclbnd 6945  faclbnd2 6946  faclbnd4lem1 6948  faclbnd4lem4 6951  bcpasc2 6967  cbvsum 6986  fsumadd 7022  fsum3 7024  fsum4 7025  csbfsumlem 7026  fsumshft 7031  fsumconst 7038  ser0mulc 7059  ser1mulc 7060  binomlem6 7071  iserzshft 7144  iserzex 7146  ser1const 7171  isumclim3t 7200  isumnn0nn 7207  isummulc1a 7214  isumsplit 7216  fnsmnt 7226  geoser 7234  geolim 7237  geolim1i 7238  geolim1 7239  fsum0diag2 7259  efseq1ex 7306  dfef2 7307  ef0lem 7310  efseq0ex 7311  erelem2 7320  erelem6 7324  ege2lem2 7328  ege2le3lem2 7329  efaddlem5 7342  efaddlem6 7343  efaddlem20 7357  efaddlem22 7359  ef1tllem 7381  eirrlem1 7389  eirrlem2 7390  eirrlem3 7391  eirrlem5 7393  efsep 7396  ef4p 7399  efm1lim 7411  efm1legeo 7417  efcnlem2 7420  efivalt 7447  sinadd 7451  cosadd 7452  cos2tOLD 7464  sin01bndlem1 7467  sin01bndlem2 7468  sin01bndlem3 7469  cos01bndlem2 7470  cos01bndlem3 7471  cos1bnd 7474  cos2bnd 7475  ruclem1 7510  ruclem2 7511  ruclem15 7524  bcthlem17 8015  bcthlem33 8031  nmcn2 8340  ipval2lem1 8351  ipval2 8357  ipid 8363  ipcj 8367  ip0r 8370  nmlnoubi 8456  nmblolbii 8459  blocnilem 8464  ip1ilem 8485  ip2i 8487  ipdirilem 8488  ipasslem10 8499  ipasslem11 8500  siilem1 8511  minveclem27 8571  minveclem38 8582  sinhalfpilem 8679  cospi 8682  eulerid 8683  sin2pi 8684  cos2pi 8685  sinperlem1 8686  sin2pim 8692  cos2pim 8693  sinmpi 8694  cosmpi 8695  sinppi 8696  sinkpi 8697  sincosq4sgn 8707  sincos4thpi 8710  sincos6thpi 8711  abssinper 8712  eff1o 8748  pilog 8768  hvmul0t 8893  hvsubass 8922  hvsub23 8923  hvsubsub4 8926  hvnegdi 8929  hvsubeq0 8930  hvsubcan2 8931  hvsubadd 8933  hvsub0t 8943  his35 8955  hisubcom 8970  normlem0 8975  normlem1 8976  normlem2 8977  normlem3 8978  normlem9 8984  norm-ii 9004  norm3dif 9014  normpar 9021  polid2 9024  polid 9025  bcsALT 9046  occllem1 9173  projlem3 9188  projlem4 9189  projlem7 9192  pjthlem5 9223  pjthlem6 9224  pjthlem7 9225  pjthlem14 9232  chdmm3 9402  chdmm4 9403  chjidmt 9443  chj4 9446  chjjdir 9447  spanunsn 9502  pjoml4 9530  cmcm2 9536  qlax4 9571  qlax5 9572  pjadj 9618  pjmul 9622  pjsub 9623  pjssm 9626  pjcj 9629  pjnel 9668  hoadd23 9704  ho0sub 9721  hosubid1t 9724  hosd2 9749  hopncan 9750  hosubeq0 9752  lnopeq0lem1 9930  lnopunilem1 9935  lnophmlem2 9942  nmbdoplb 9949  nmcopexlem2 9952  lnfnmul 9973  nmcfnexlem2 9981  nmoptri2 10032  nmopcoadj 10034  golem1 10198  mdsl1 10248  cvmd 10251  mdslmd3 10259  csmdsym 10261  1cat 10692

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703  ax-pow 2742  ax-pr 2779

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413  df-op 2416  df-uni 2504  df-br 2620  df-opab 2667  df-xp 3184  df-cnv 3186  df-dm 3188  df-rn 3189  df-res 3190  df-ima 3191  df-fv 3198  df-opr 3965

Copyright terms: Public domain