Theorem opreq2i 4704

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

Syntax hints:   = wceq 1136  (class class class)co 4695

This theorem is referenced by:  opreq12iOLD 4706  caopr32 4804  caopr4 4808  caopr42 4810  oa1suc 5020  om1 5034  oe1 5036  oawordeulem 5047  oeoalem 5082  nneob 5123  cdaassen 5876  mapcdaen 5878  addasspq 6011  mulidpq 6017  addclprlem2 6067  prlem934a 6085  prlem936a 6101  mulcmpblnrlem 6130  m1p1sr 6149  m1m1sr 6150  0idsr 6154  1idsr 6155  00sr 6156  pn0sr 6158  recexsrlem 6160  mulgt0sr 6162  sqgt0sr 6163  mappsrpr 6166  supsrlem2 6174  supsrlem5 6177  mulresr 6205  axmulcom 6225  axmulass 6227  axdistr 6228  ax0id 6230  ax1id 6231  axi2m1 6234  axcnre 6235  add42i 6293  negid 6332  negsubi 6334  negsubiOLD 6335  negnegiOLD 6346  neg11i 6362  mul01i 6390  negsubdii 6409  ltsubaddiOLD 6566  ltnegi 6579  ixiOLD 6669  muleqadd 6685  divreci 6716  recreci 6741  rec11ii 6749  2p2e4 6980  3p2e5 6986  3p3e6 6987  4p2e6 6988  4p3e7 6989  4p4e8 6990  5p2e7 6991  5p3e8 6992  5p4e9 6993  5p5e10 6994  6p2e8 6995  6p3e9 6996  6p4e10 6997  7p2e9 6998  7p3e10 6999  8p2e10 7000  3t3e9 7003  8th4div3 7012  halfpm6th 7013  halfpos 7017  addltmul 7024  nneoi 7204  zeo 7206  quoremz 7287  quoremnn0 7289  intfrac2 7290  intfracq 7291  fztp 7481  fzprval 7482  fztpval 7483  fzshftral 7496  shftidt 7563  seq1seqz 7579  seq0seqz 7580  seq1seq01 7582  seqzres2 7599  expp1 7612  sqval 7649  sqrecii 7659  cu2 7680  binom2i 7685  discrlem1 7701  discrlem3 7703  nnesqi 7707  nn0opthlem1 7709  sqrlem2 7719  sqrlem11 7728  sqr2irrlem1 7769  i3 7778  i4 7779  crulem 7781  crmuli 7785  crreczi 7786  cjcji 7823  recji 7827  imcji 7828  readdi 7829  imaddi 7830  cjaddi 7833  cjmuli 7834  ipcni 7835  cjmulrcli 7836  renegi 7839  imnegi 7841  cjnegi 7842  addcji 7843  cji 7872  absmuli 7893  absidi 7907  absi 7925  cjdivi 7935  abstrii 7938  abslem2i 7955  faclbnd 7992  faclbnd2 7993  faclbnd4lem1 7995  faclbnd4lem4 7998  bcpasc2i 8014  cbvsumi 8041  fsumadd 8077  fsum3 8079  fsum4 8080  csbfsumlem 8081  fsumshft 8086  fsumconst 8093  ser0mulci 8114  ser1mulci 8115  binomlem6 8126  iserzshfti 8199  iserzexi 8201  ser1consti 8226  isumclim3 8256  isumnn0nn 8263  isummulc1ai 8270  isumspliti 8272  arisumi 8282  geoseri 8291  geolim 8294  geolim1i 8295  geolim1 8296  fsum0diag2 8316  efseq1ex 8363  dfef2i 8364  ef0lem 8367  efseq0ex 8368  erelem2 8377  erelem6 8381  ege2lem2 8385  ege2le3lem2 8386  efaddlem5 8399  efaddlem6 8400  efaddlem20 8414  efaddlem22 8416  ef1tllem 8438  eirrlem1 8446  eirrlem2 8447  eirrlem3 8448  eirrlem5 8450  efsepi 8456  ef4pi 8459  efm1limi 8471  efm1legeoi 8477  efcnlem2 8480  efival 8507  sinaddi 8511  cosaddi 8512  cos2OLD 8525  sin01bndlem1 8528  sin01bndlem2 8529  sin01bndlem3 8530  cos01bndlem2 8531  cos01bndlem3 8532  cos1bnd 8535  cos2bnd 8536  ruclem1 8574  ruclem2 8575  ruclem15 8588  bcthlem17 9088  bcthlem33 9104  nmcn2 9474  ipval2lem1 9485  ipval2 9491  ipid 9497  ipcj 9501  ip0r 9504  nmlnoubi 9591  nmblolbii 9594  blocnilem 9599  ip1ilem 9621  ip2i 9623  ipdirilem 9624  ipasslem10 9635  ipasslem11 9636  siilem1 9647  minveclem27 9711  minveclem38 9722  sinhalfpilem 9823  cospi 9826  eulerid 9827  sin2pi 9828  cos2pi 9829  sinperlem1 9830  sin2pim 9836  cos2pim 9837  sinmpi 9838  cosmpi 9839  sinppi 9840  cosppi 9841  sincosq4sgn 9851  sincos4thpi 9855  sincos6thpi 9856  abssinper 9857  eff1o 9897  pilog 9917  hvmul0 10317  hvsubassi 10346  hvsub23i 10347  hvsubsub4i 10350  hvnegdii 10353  hvsubeq0i 10354  hvsubcan2i 10355  hvsubaddi 10357  hvsub0 10368  his35i 10380  hisubcomi 10395  normlem0 10400  normlem1 10401  normlem2 10402  normlem3 10403  normlem9 10409  norm-ii.i 10429  norm3difi 10439  normpari 10446  polid2i 10449  polidi 10450  bcsiALT 10471  occllem1 10598  projlem3 10613  projlem4 10614  projlem7 10617  pjthlem5 10648  pjthlem6 10649  pjthlem7 10650  pjthlem14 10657  chdmm3i 10827  chdmm4i 10828  chjidm 10868  chj4i 10871  chjjdiri 10872  spanunsni 10927  pjoml4i 10955  cmcm2i 10961  qlax4i 10998  qlax5i 10999  pjadjii 11045  pjmulii 11049  pjsubii 11050  pjssmii 11053  pjcji 11056  pjneli 11095  hoadd23i 11133  ho0subi 11150  hosubid1 11153  hosd2i 11178  hopncani 11179  hosubeq0i 11181  lnopeq0lem1 11359  lnopunilem1 11364  lnophmlem2 11371  nmbdoplbi 11378  nmcopexlem2 11381  lnfnmuli 11402  nmcfnexlem2 11410  nmoptri2i 11461  nmopcoadji 11463  golem1 11635  mdsl1i 11685  cvmdi 11688  mdslmd3i 11696  csmdsymi 11698  divalglem5 13492  divalglem6 13493  gcdaddmlem 13526  mulgcdlem2 13549  mulgcdlem5 13552  3prm 13572  geme2 14341  nfwpr4c 14355  tolat 14356  cbvprodi 14386  cntrsetlem 14709  1cat 14788  ivthALT 15136  fsumleisumi 15508  trirni 15515  geomcau 15531  bfplem6 15685  ismrer1 15706  reheibor 15707  phtpycom 15732  phtpyco 15738  reparphtlem2 15746  pcoass 15767  pcorevlem 15768  stb2xpl 16501  stb3xpl 16502

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1142  ax-gen 1143  ax-8 1144  ax-9 1145  ax-10 1146  ax-11 1147  ax-12 1148  ax-14 1150  ax-17 1155  ax-4 1157  ax-5o 1159  ax-6o 1162  ax-9o 1319  ax-10o 1338  ax-16 1418  ax-11o 1426  ax-ext 1702  ax-sep 3253  ax-nul 3260  ax-pow 3296  ax-pr 3339

This theorem depends on definitions:  df-bi 163  df-or 240  df-an 241  df-ex 1165  df-sb 1374  df-eu 1613  df-mo 1614  df-clab 1709  df-cleq 1714  df-clel 1717  df-ne 1856  df-rex 1944  df-v 2127  df-dif 2430  df-un 2433  df-in 2436  df-ss 2438  df-nul 2702  df-pw 2859  df-sn 2873  df-pr 2874  df-op 2877  df-uni 3000  df-br 3159  df-opab 3214  df-xp 3811  df-cnv 3813  df-dm 3815  df-rn 3816  df-res 3817  df-ima 3818  df-fv 3825  df-opr 4697

Copyright terms: Public domain