Theorem opreq2i 3978

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 3975	. 2 |- (A = B -> (CFA) = (CFB))
3	1, 2	ax-mp 7	1 |- (CFA) = (CFB)

Syntax hints:   = wceq 958  (class class class)co 3969

This theorem is referenced by:  opreq12i 3979  caopr32 4066  caopr4 4070  caopr42 4072  oa1suc 4170  om1 4182  oe1 4184  oawordeulem 4194  nneob 4261  cdaassen 4942  mapcdaen 4944  addasspq 5075  mulidpq 5081  addclprlem2 5131  prlem934a 5149  prlem936a 5165  mulcmpblnrlem 5194  m1p1sr 5213  m1m1sr 5214  0idsr 5218  1idsr 5219  00sr 5220  pn0sr 5222  recexsrlem 5224  mulgt0sr 5226  sqgt0sr 5227  mappsrpr 5230  supsrlem2 5238  supsrlem5 5241  mulresr 5269  axmulcom 5288  axmulass 5290  axdistr 5291  ax0id 5293  ax1id 5294  axi2m1 5297  axcnre 5298  add42 5355  negidt 5391  negsub 5393  negneg 5402  neg11 5418  mul01 5443  negsubdi 5461  ltsubadd 5606  ltneg 5615  ixi 5693  muleqaddt 5712  divrec 5744  recrec 5770  rec11i 5779  2p2e4 6003  3p2e5 6009  3p3e6 6010  4p2e6 6011  4p3e7 6012  4p4e8 6013  5p2e7 6014  5p3e8 6015  5p4e9 6016  5p5e10 6017  6p2e8 6018  6p3e9 6019  6p4e10 6020  7p2e9 6021  7p3e10 6022  8p2e10 6023  3t3e9 6026  8th4div3 6033  halfpm6th 6034  halfpost 6038  nneo 6199  zeot 6201  quoremz 6253  intfrac 6254  intfracq 6255  shftidt 6356  fzshftralt 6523  seq1seqz 6542  seq0seqz 6543  seq1seq0t 6545  seqzres2 6562  expp1t 6575  sqvalt 6610  sqreci 6620  cu2 6641  binom2 6645  discrlem1 6657  discrlem3 6659  nnesq 6663  nn0opthlem1 6665  sqrlem2 6675  sqrlem11 6684  sqr2irrlem1 6725  i3 6734  i4 6735  crulem 6737  crmul 6741  crrecz 6742  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 7465  sin01bndlem1 7468  sin01bndlem2 7469  sin01bndlem3 7470  cos01bndlem2 7471  cos01bndlem3 7472  cos1bnd 7475  cos2bnd 7476  ruclem1 7511  ruclem2 7512  ruclem15 7525  bcthlem17 8012  bcthlem33 8028  nmcn2 8336  ipval2lem1 8347  ipval2 8353  ipid 8359  ipcj 8363  ip0r 8366  nmlnoubi 8452  nmblolbii 8455  blocnilem 8460  ip1ilem 8481  ip2i 8483  ipdirilem 8484  ipasslem10 8495  ipasslem11 8496  siilem1 8507  minveclem27 8567  minveclem38 8578  sinhalfpilem 8674  cospi 8677  eulerid 8678  sin2pi 8679  cos2pi 8680  sinperlem1 8681  sin2pim 8687  cos2pim 8688  sinmpi 8689  cosmpi 8690  sinppi 8691  sinkpi 8692  sincosq4sgn 8702  sincos4thpi 8705  sincos6thpi 8706  abssinper 8707  eff1o 8743  pilog 8763  hvmul0t 8888  hvsubass 8917  hvsub23 8918  hvsubsub4 8921  hvnegdi 8924  hvsubeq0 8925  hvsubcan2 8926  hvsubadd 8928  hvsub0t 8938  his35 8950  hisubcom 8965  normlem0 8970  normlem1 8971  normlem2 8972  normlem3 8973  normlem9 8979  norm-ii 8999  norm3dif 9009  normpar 9016  polid2 9019  polid 9020  bcsALT 9041  occllem1 9168  projlem3 9183  projlem4 9184  projlem7 9187  pjthlem5 9218  pjthlem6 9219  pjthlem7 9220  pjthlem14 9227  chdmm3 9397  chdmm4 9398  chjidmt 9438  chj4 9441  chjjdir 9442  spanunsn 9497  pjoml4 9525  cmcm2 9531  qlax4 9566  qlax5 9567  pjadj 9613  pjmul 9617  pjsub 9618  pjssm 9621  pjcj 9624  pjnel 9663  hoadd23 9699  ho0sub 9716  hosubid1t 9719  hosd2 9744  hopncan 9745  hosubeq0 9747  lnopeq0lem1 9925  lnopunilem1 9930  lnophmlem2 9937  nmbdoplb 9944  nmcopexlem2 9947  lnfnmul 9968  nmcfnexlem2 9976  nmoptri2 10027  nmopcoadj 10029  golem1 10193  mdsl1 10243  cvmd 10246  mdslmd3 10254  csmdsym 10256  1cat 10663

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-sep 2708  ax-pow 2748  ax-pr 2785

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-v 1815  df-dif 2052  df-un 2053  df-in 2054  df-ss 2056  df-nul 2284  df-pw 2406  df-sn 2416  df-pr 2417  df-op 2420  df-uni 2508  df-br 2625  df-opab 2672  df-xp 3190  df-cnv 3192  df-dm 3194  df-rn 3195  df-res 3196  df-ima 3197  df-fv 3204  df-opr 3971

Copyright terms: Public domain