Theorem opreq2i 3957

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

Syntax hints:   = wceq 953  (class class class)co 3948

This theorem is referenced by:  opreq12i 3958  caopr32 4046  caopr4 4050  caopr42 4052  oa1suc 4148  om1 4160  oe1 4162  oawordeulem 4172  nneob 4239  cdaassen 4902  mapcdaen 4904  addasspq 5035  mulidpq 5041  addclprlem2 5091  prlem934a 5109  prlem936a 5125  mulcmpblnrlem 5154  m1p1sr 5173  m1m1sr 5174  0idsr 5178  1idsr 5179  00sr 5180  pn0sr 5182  recexsrlem 5184  mulgt0sr 5186  sqgt0sr 5187  mappsrpr 5190  supsrlem2 5198  supsrlem5 5201  mulresr 5229  axmulcom 5248  axmulass 5250  axdistr 5251  ax0id 5253  ax1id 5254  axi2m1 5257  axcnre 5258  add42 5315  negidt 5351  negsub 5353  negneg 5362  neg11 5378  mul01 5403  negsubdi 5421  ltsubadd 5568  ltneg 5577  ixi 5654  muleqaddt 5669  divrec 5700  recrec 5725  rec11i 5733  2p2e4 5948  3p2e5 5954  3p3e6 5955  4p2e6 5956  4p3e7 5957  4p4e8 5958  5p2e7 5959  5p3e8 5960  5p4e9 5961  5p5e10 5962  6p2e8 5963  6p3e9 5964  6p4e10 5965  7p2e9 5966  7p3e10 5967  8p2e10 5968  3t3e9 5971  8th4div3 5978  halfpm6th 5979  halfpost 5983  nneo 6144  zeot 6146  shftidt 6292  fzshftralt 6454  seq1seqz 6473  seq0seqz 6474  seq1seq0t 6476  seqzres2 6493  expp1t 6506  sqvalt 6540  sqreci 6549  cu2 6571  binom2 6575  discrlem1 6586  discrlem3 6588  nnesq 6592  nn0opthlem1 6594  sqrlem2 6604  sqrlem11 6613  sqr2irrlem1 6654  i3 6663  i4 6664  crulem 6666  crmul 6671  crrecz 6672  imret 6710  cjcj 6713  recj 6717  imcj 6718  readd 6719  imadd 6720  cjadd 6723  cjmul 6724  ipcn 6725  cjmulrcl 6726  reneg 6729  imneg 6731  cjneg 6732  addcj 6733  cji 6762  absmul 6782  absid 6796  absi 6815  cjdiv 6826  abstri 6829  abslem2i 6845  faclbnd 6882  faclbnd2 6883  faclbnd4lem1 6885  faclbnd4lem4 6888  bcpasc2 6905  cbvsum 6924  fsumadd 6960  fsum3 6962  fsum4 6963  csbfsumlem 6964  fsumshft 6969  fsumconst 6976  ser0mulc 6997  ser1mulc 6998  binomlem6 7009  iserzshft 7080  iserzex 7082  ser1const 7107  isumclim3t 7135  isumnn0nn 7142  isummulc1a 7149  isumsplit 7151  fnsmnt 7161  geoser 7169  geolim 7172  geolim1i 7173  geolim1 7174  fsum0diag2 7194  efseq1ex 7248  dfef2 7249  ef0lem 7252  efseq0ex 7253  erelem2 7262  erelem6 7266  ege2lem2 7270  ege2le3lem2 7271  efaddlem5 7284  efaddlem6 7285  efaddlem20 7299  efaddlem22 7301  ef1tllem 7323  eirrlem1 7330  eirrlem2 7331  eirrlem3 7332  eirrlem5 7334  efsep 7337  ef4p 7340  efm1lim 7351  efm1legeo 7357  efcnlem2 7360  efivalt 7389  sinadd 7393  cosadd 7394  cos2tOLD 7406  sin01bndlem1 7409  sin01bndlem2 7410  sin01bndlem3 7411  cos01bndlem2 7412  cos01bndlem3 7413  cos1bnd 7416  cos2bnd 7417  ruclem1 7453  ruclem2 7454  ruclem15 7467  bcthlem17 7949  bcthlem33 7965  nmcn2 8275  ipval2lem1 8285  ipval2 8291  ipid 8297  ipcj 8301  ip0r 8304  nmlnoubi 8388  nmblolbii 8390  blocnilem 8395  ip1ilem 8416  ip2i 8418  ipdirilem 8419  ipasslem10 8430  ipasslem11 8431  siilem1 8442  minveclem27 8502  minveclem38 8513  sinhalfpilem 8598  cospi 8601  eulerid 8602  sin2pi 8603  cos2pi 8604  sinperlem1 8605  sin2pim 8611  cos2pim 8612  sinmpi 8613  cosmpi 8614  sincosq4sgn 8624  sincos4thpi 8627  sincos6thpi 8628  eff1o 8670  pilog 8690  hvmul0t 8814  hvsubass 8843  hvsub23 8844  hvsubsub4 8847  hvnegdi 8850  hvsubeq0 8851  hvsubcan2 8852  hvsubadd 8854  hvsub0t 8864  his35 8876  hisubcom 8891  normlem0 8896  normlem1 8897  normlem2 8898  normlem3 8899  normlem9 8905  norm-ii 8925  norm3dif 8935  normpar 8942  polid2 8945  polid 8946  bcsALT 8967  occllem1 9089  projlem3 9104  projlem4 9105  projlem7 9108  pjthlem5 9138  pjthlem6 9139  pjthlem7 9140  pjthlem14 9147  chdmm3 9317  chdmm4 9318  chjidmt 9358  chj4 9361  chjjdir 9362  spanunsn 9419  pjoml4 9447  cmcm2 9453  qlax4 9488  qlax5 9489  pjadj 9535  pjmul 9539  pjsub 9540  pjssm 9543  pjcj 9546  pjnel 9585  hoadd23 9621  ho0sub 9638  hosubid1t 9641  hosd2 9666  hopncan 9667  hosubeq0 9669  lnopeq0lem1 9845  lnopunilem1 9850  lnophmlem2 9857  nmbdoplb 9864  nmcopexlem2 9867  lnfnmul 9888  nmcfnexlem2 9896  nmoptri2 9946  nmopcoadj 9948  golem1 10108  mdsl1 10156  cvmd 10159  mdslmd3 10167  csmdsym 10169  1cat 10536

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-pow 2732  ax-pr 2769

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403  df-op 2406  df-uni 2494  df-br 2610  df-opab 2657  df-xp 3174  df-cnv 3176  df-dm 3178  df-rn 3179  df-res 3180  df-ima 3181  df-fv 3188  df-opr 3950

Copyright terms: Public domain