Theorem opreq2i 3963

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

Syntax hints:   = wceq 954  (class class class)co 3954

This theorem is referenced by:  opreq12i 3964  caopr32 4052  caopr4 4056  caopr42 4058  oa1suc 4154  om1 4166  oe1 4168  oawordeulem 4178  nneob 4245  cdaassen 4910  mapcdaen 4912  addasspq 5043  mulidpq 5049  addclprlem2 5099  prlem934a 5117  prlem936a 5133  mulcmpblnrlem 5162  m1p1sr 5181  m1m1sr 5182  0idsr 5186  1idsr 5187  00sr 5188  pn0sr 5190  recexsrlem 5192  mulgt0sr 5194  sqgt0sr 5195  mappsrpr 5198  supsrlem2 5206  supsrlem5 5209  mulresr 5237  axmulcom 5256  axmulass 5258  axdistr 5259  ax0id 5261  ax1id 5262  axi2m1 5265  axcnre 5266  add42 5323  negidt 5359  negsub 5361  negneg 5370  neg11 5386  mul01 5411  negsubdi 5429  ltsubadd 5576  ltneg 5585  ixi 5662  muleqaddt 5677  divrec 5708  recrec 5733  rec11i 5741  2p2e4 5956  3p2e5 5962  3p3e6 5963  4p2e6 5964  4p3e7 5965  4p4e8 5966  5p2e7 5967  5p3e8 5968  5p4e9 5969  5p5e10 5970  6p2e8 5971  6p3e9 5972  6p4e10 5973  7p2e9 5974  7p3e10 5975  8p2e10 5976  3t3e9 5979  8th4div3 5986  halfpm6th 5987  halfpost 5991  nneo 6152  zeot 6154  shftidt 6300  fzshftralt 6462  seq1seqz 6481  seq0seqz 6482  seq1seq0t 6484  seqzres2 6501  expp1t 6514  sqvalt 6548  sqreci 6557  cu2 6579  binom2 6583  discrlem1 6594  discrlem3 6596  nnesq 6600  nn0opthlem1 6602  sqrlem2 6612  sqrlem11 6621  sqr2irrlem1 6662  i3 6671  i4 6672  crulem 6674  crmul 6679  crrecz 6680  imret 6718  cjcj 6721  recj 6725  imcj 6726  readd 6727  imadd 6728  cjadd 6731  cjmul 6732  ipcn 6733  cjmulrcl 6734  reneg 6737  imneg 6739  cjneg 6740  addcj 6741  cji 6770  absmul 6790  absid 6804  absi 6823  cjdiv 6834  abstri 6837  abslem2i 6853  faclbnd 6890  faclbnd2 6891  faclbnd4lem1 6893  faclbnd4lem4 6896  bcpasc2 6913  cbvsum 6932  fsumadd 6968  fsum3 6970  fsum4 6971  csbfsumlem 6972  fsumshft 6977  fsumconst 6984  ser0mulc 7005  ser1mulc 7006  binomlem6 7017  iserzshft 7088  iserzex 7090  ser1const 7115  isumclim3t 7143  isumnn0nn 7150  isummulc1a 7157  isumsplit 7159  fnsmnt 7169  geoser 7177  geolim 7180  geolim1i 7181  geolim1 7182  fsum0diag2 7202  efseq1ex 7256  dfef2 7257  ef0lem 7260  efseq0ex 7261  erelem2 7270  erelem6 7274  ege2lem2 7278  ege2le3lem2 7279  efaddlem5 7292  efaddlem6 7293  efaddlem20 7307  efaddlem22 7309  ef1tllem 7331  eirrlem1 7338  eirrlem2 7339  eirrlem3 7340  eirrlem5 7342  efsep 7345  ef4p 7348  efm1lim 7359  efm1legeo 7365  efcnlem2 7368  efivalt 7397  sinadd 7401  cosadd 7402  cos2tOLD 7414  sin01bndlem1 7417  sin01bndlem2 7418  sin01bndlem3 7419  cos01bndlem2 7420  cos01bndlem3 7421  cos1bnd 7424  cos2bnd 7425  ruclem1 7461  ruclem2 7462  ruclem15 7475  bcthlem17 7965  bcthlem33 7981  nmcn2 8288  ipval2lem1 8298  ipval2 8304  ipid 8310  ipcj 8314  ip0r 8317  nmlnoubi 8401  nmblolbii 8403  blocnilem 8408  ip1ilem 8429  ip2i 8431  ipdirilem 8432  ipasslem10 8443  ipasslem11 8444  siilem1 8455  minveclem27 8515  minveclem38 8526  sinhalfpilem 8617  cospi 8620  eulerid 8621  sin2pi 8622  cos2pi 8623  sinperlem1 8624  sin2pim 8630  cos2pim 8631  sinmpi 8632  cosmpi 8633  sincosq4sgn 8643  sincos4thpi 8646  sincos6thpi 8647  eff1o 8687  pilog 8707  hvmul0t 8832  hvsubass 8861  hvsub23 8862  hvsubsub4 8865  hvnegdi 8868  hvsubeq0 8869  hvsubcan2 8870  hvsubadd 8872  hvsub0t 8882  his35 8894  hisubcom 8909  normlem0 8914  normlem1 8915  normlem2 8916  normlem3 8917  normlem9 8923  norm-ii 8943  norm3dif 8953  normpar 8960  polid2 8963  polid 8964  bcsALT 8985  occllem1 9112  projlem3 9127  projlem4 9128  projlem7 9131  pjthlem5 9161  pjthlem6 9162  pjthlem7 9163  pjthlem14 9170  chdmm3 9340  chdmm4 9341  chjidmt 9381  chj4 9384  chjjdir 9385  spanunsn 9442  pjoml4 9470  cmcm2 9476  qlax4 9511  qlax5 9512  pjadj 9558  pjmul 9562  pjsub 9563  pjssm 9566  pjcj 9569  pjnel 9608  hoadd23 9644  ho0sub 9661  hosubid1t 9664  hosd2 9689  hopncan 9690  hosubeq0 9692  lnopeq0lem1 9868  lnopunilem1 9873  lnophmlem2 9880  nmbdoplb 9887  nmcopexlem2 9890  lnfnmul 9911  nmcfnexlem2 9919  nmoptri2 9970  nmopcoadj 9972  golem1 10136  mdsl1 10185  cvmd 10188  mdslmd3 10196  csmdsym 10198  1cat 10572

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698  ax-pow 2737  ax-pr 2774

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409  df-op 2412  df-uni 2499  df-br 2615  df-opab 2662  df-xp 3179  df-cnv 3181  df-dm 3183  df-rn 3184  df-res 3185  df-ima 3186  df-fv 3193  df-opr 3956

Copyright terms: Public domain