Theorem opreq2i 3911

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

Syntax hints:   = wceq 1099  (class class class)co 3902

This theorem is referenced by:  opreq12i 3912  caopr32 4000  caopr4 4004  caopr42 4006  oa1suc 4102  om1 4114  oe1 4116  oawordeulem 4126  nneob 4193  cdaassen 4853  mapcdaen 4855  addasspq 4986  mulidpq 4992  addclprlem2 5042  prlem934a 5060  prlem936a 5076  mulcmpblnrlem 5105  m1p1sr 5124  m1m1sr 5125  0idsr 5129  1idsr 5130  00sr 5131  pn0sr 5133  recexsrlem 5135  mulgt0sr 5137  sqgt0sr 5138  mappsrpr 5141  supsrlem2 5149  supsrlem5 5152  mulresr 5180  axmulcom 5199  axmulass 5201  axdistr 5202  ax0id 5204  ax1id 5205  axi2m1 5208  axcnre 5209  add42 5266  negidt 5302  negsub 5304  negneg 5313  neg11 5329  mul01 5354  negsubdi 5372  ltsubadd 5519  ltneg 5528  ixi 5605  muleqaddt 5620  divrec 5651  recrec 5676  rec11i 5684  2p2e4 5899  3p2e5 5905  3p3e6 5906  4p2e6 5907  4p3e7 5908  4p4e8 5909  5p2e7 5910  5p3e8 5911  5p4e9 5912  5p5e10 5913  6p2e8 5914  6p3e9 5915  6p4e10 5916  7p2e9 5917  7p3e10 5918  8p2e10 5919  3t3e9 5922  8th4div3 5929  halfpm6th 5930  halfpost 5934  nneo 6095  zeot 6097  shftidt 6243  fzshftralt 6405  seq1seqz 6424  seq0seqz 6425  seq1seq0t 6427  seqzres2 6444  expp1t 6457  sqvalt 6491  sqreci 6500  cu2 6522  binom2 6526  discrlem1 6537  discrlem3 6539  nnesq 6543  nn0opthlem1 6545  sqrlem2 6555  sqrlem11 6564  sqr2irrlem1 6605  i3 6614  i4 6615  crulem 6617  crmul 6622  crrecz 6623  imret 6661  cjcj 6664  recj 6668  imcj 6669  readd 6670  imadd 6671  cjadd 6674  cjmul 6675  ipcn 6676  cjmulrcl 6677  reneg 6680  imneg 6682  cjneg 6683  addcj 6684  cji 6713  absmul 6733  absid 6747  absi 6766  cjdiv 6777  abstri 6780  abslem2i 6796  faclbnd 6833  faclbnd2 6834  faclbnd4lem1 6836  faclbnd4lem4 6839  bcpasc2 6856  cbvsum 6875  fsumadd 6911  fsum3 6913  fsum4 6914  csbfsumlem 6915  fsumshft 6920  fsumconst 6927  ser0mulc 6948  ser1mulc 6949  binomlem6 6960  iserzshft 7031  iserzex 7033  ser1const 7058  isumclim3t 7086  isumnn0nn 7093  isummulc1a 7100  isumsplit 7102  fnsmnt 7112  geoser 7120  geolim 7123  geolim1i 7124  geolim1 7125  fsum0diag2 7145  efseq1ex 7199  dfef2 7200  ef0lem 7203  efseq0ex 7204  erelem2 7213  erelem6 7217  ege2lem2 7221  ege2le3lem2 7222  efaddlem5 7235  efaddlem6 7236  efaddlem20 7250  efaddlem22 7252  ef1tllem 7274  eirrlem1 7281  eirrlem2 7282  eirrlem3 7283  eirrlem5 7285  efsep 7288  ef4p 7291  efm1lim 7302  efm1legeo 7308  efcnlem2 7311  efivalt 7340  sinadd 7344  cosadd 7345  cos2tOLD 7357  sin01bndlem1 7360  sin01bndlem2 7361  sin01bndlem3 7362  cos01bndlem2 7363  cos01bndlem3 7364  cos1bnd 7367  cos2bnd 7368  ruclem1 7404  ruclem2 7405  ruclem15 7418  bcthlem17 7897  bcthlem33 7913  nmcn2 8212  ipval2lem1 8220  ipval2 8226  ipid 8232  ipcj 8236  ip0r 8239  nmlnoubi 8323  nmblolbii 8325  blocnilem 8330  ip1ilem 8351  ip2i 8353  ipdirilem 8354  ipasslem10 8365  ipasslem11 8366  siilem1 8377  minveclem27 8437  minveclem38 8448  sinhalfpilem 8511  cospi 8514  eulerid 8515  sin2pi 8516  cos2pi 8517  sinperlem1 8518  sin2pim 8524  cos2pim 8525  sinmpi 8526  cosmpi 8527  sincosq4sgn 8537  sincos4thpi 8540  sincos6thpi 8541  eff1o 8583  pilog 8603  1cat 8886  hvmul0t 9042  hvsubass 9071  hvsub23 9072  hvsubsub4 9075  hvnegdi 9078  hvsubeq0 9079  hvsubcan2 9080  hvsubadd 9082  hvsub0t 9092  his35 9104  hisubcom 9119  normlem0 9124  normlem1 9125  normlem2 9126  normlem3 9127  normlem9 9133  norm-ii 9153  norm3dif 9163  normpar 9170  polid2 9173  polid 9174  bcsALT 9195  occllem1 9303  projlem3 9318  projlem4 9319  projlem7 9322  pjthlem5 9352  pjthlem6 9353  pjthlem7 9354  pjthlem14 9361  chdmm3 9531  chdmm4 9532  chjidmt 9572  chj4 9575  chjjdir 9576  spanunsn 9633  pjoml4 9661  cmcm2 9667  qlax4 9702  qlax5 9703  pjadj 9749  pjmul 9753  pjsub 9754  pjssm 9757  pjcj 9760  pjnel 9799  hoadd23 9835  ho0sub 9852  hosubid1t 9855  hosd2 9880  hopncan 9881  hosubeq0 9883  lnopeq0lem1 10059  lnopunilem1 10064  lnophmlem2 10071  nmbdoplb 10078  nmcopexlem2 10081  lnfnmul 10102  nmcfnexlem2 10110  nmoptri2 10160  nmopcoadj 10162  golem1 10322  mdsl1 10370  cvmd 10373  mdslmd3 10381  csmdsym 10383

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-13 1107  ax-14 1108  ax-11 1180  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436  ax-sep 2671  ax-pow 2710  ax-pr 2747

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 957  df-sb 1155  df-eu 1359  df-mo 1360  df-clab 1441  df-cleq 1446  df-clel 1449  df-ne 1563  df-v 1787  df-dif 2020  df-un 2021  df-in 2022  df-ss 2024  df-nul 2252  df-pw 2373  df-sn 2383  df-pr 2384  df-op 2387  df-uni 2472  df-br 2588  df-opab 2635  df-xp 3147  df-cnv 3149  df-dm 3151  df-rn 3152  df-res 3153  df-ima 3154  df-fv 3161  df-opr 3904

Copyright terms: Public domain