Theorem opreq1i 4029

Description: Equality inference for operation value.

Hypothesis

Ref	Expression
opreq1i.1	|- A = B

Assertion

Ref	Expression
opreq1i	|- (AFC) = (BFC)

Proof of Theorem opreq1i

Step	Hyp	Ref	Expression
1		opreq1i.1	. 2 |- A = B
2		opreq1 4026	. 2 |- (A = B -> (AFC) = (BFC))
3	1, 2	ax-mp 7	1 |- (AFC) = (BFC)

Syntax hints:   = wceq 992  (class class class)co 4021

This theorem is referenced by:  opreq12i 4031  caopr12 4122  caopr411 4126  map1 4571  cdaassen 5082  distrpq 5221  ltapq 5230  ltmpq 5231  ltexpq 5234  halfpq 5236  addclprlem2 5273  prlem934a 5291  m1m1sr 5356  recexsrlem 5366  axi2m1 5439  axcnre 5440  negnegi 5544  mul12i 5577  mulneg1i 5599  ltnegi 5757  ixi 5837  recextlem1 5838  div23i 5894  divcan4i 5898  divcan4zi 5900  recreci 5908  rec11ii 5916  divmul13i 5926  recdiv 5929  divdiv23i 5932  prodgt0lem 5958  nnsubi 6102  2p2e4 6147  2timesi 6149  3p2e5 6153  3p3e6 6154  4p2e6 6155  4p3e7 6156  4p4e8 6157  5p2e7 6158  5p3e8 6159  5p4e9 6160  5p5e10 6161  6p2e8 6162  6p3e9 6163  6p4e10 6164  7p2e9 6165  7p3e10 6166  8p2e10 6167  8th4div3 6177  halfpm6th 6178  nneoi 6368  uzindOLD 6379  quoremz 6451  quoremnn0 6453  om2uzsuci 6659  exprec 6789  exprecOLD 6790  sqrecii 6816  cu2 6837  binom2i 6841  binom2aiOLD 6842  discrlem1 6857  nnesqi 6863  nn0opthlem1 6865  nn0opth2i 6868  sqrlem11 6884  sqrlem16 6889  i3 6934  crulem 6937  crmuli 6941  crreczi 6942  rimul 6945  imre 6974  cjdivi 7091  abslem2i 7111  faclbnd 7148  bcpasc2i 7170  fsump1fi 7214  binomlem1 7269  binomlem2 7270  binomlem4 7272  binomlem6 7274  iserzshfti 7347  isumnn0nn 7411  arisumilem 7429  arisumi 7430  geoseri 7439  geolimilem 7440  geolim1i 7443  georeclim 7445  geoisumr 7448  cvgratlem1ALT 7452  cvgratlem3ALT 7454  efseq0ex 7516  efaddlem5 7547  efaddlem6 7548  efaddlem16 7558  efaddlem20 7562  efaddlem22 7564  efnn0val 7578  ef1tllem 7586  eirrlem3 7596  abspef01tlubi 7603  efm1limi 7619  efm1legeoi 7625  efcnlem2 7628  resinval 7641  recosval 7642  efi4p 7643  efival 7655  sinaddi 7659  cosaddi 7660  cos2tsin 7672  cos2OLD 7673  sin01bndlem1 7676  sin01bndlem2 7677  cos01bndlem2 7679  cos1bnd 7683  cos2bnd 7684  absefib 7693  efieq1re 7694  demoivre 7695  acdc3lem 7697  acdc2lem2 7701  acdc5lem2 7704  acdclem 7706  infpnlem1 7718  ruclem1 7722  ruclem2 7723  ruclem3 7724  ruclem15 7736  fsumcnlem 8200  vc2 8421  vc0 8435  vcm 8437  vcnegneg 8440  nvnncan 8530  nvm1 8539  nvpi 8541  nvmtri 8546  nvge0 8549  ipval2lem1 8605  ipval2 8611  ipval3 8613  ipid 8617  ip0i 8740  ip1ilem 8741  ip2i 8743  ipdirilem 8744  ipasslem10 8755  siilem1 8767  siii 8769  minveclem19 8823  minveclem27 8831  minveclem35 8839  minveclem38 8842  sinhalfpilem 8946  cospi 8949  eulerid 8950  cos2pi 8952  sinperlem1 8953  sinhalfpip 8966  sinhalfpim 8967  coshalfpip 8968  coshalfpim 8969  sincosq3sgn 8973  sincosq4sgn 8974  sincos4thpi 8978  sincos6thpi 8979  sineq0re 8985  pilog 9040  hvsubid 9170  hvaddsubval 9177  hvmul2negi 9190  hvsubassi 9197  hvadd12i 9199  hv2times 9203  hvnegdii 9204  hvaddcani 9207  hi01 9238  hisubcomi 9246  normlem0 9251  normlem1 9252  normlem3 9254  normlem9 9260  bcseqi 9262  normsqi 9275  norm-ii.i 9280  normsubi 9284  norm3difi 9290  norm3adifii 9291  normpar2i 9299  polid2i 9300  polidi 9301  occllem1 9449  projlem3 9464  projlem4 9465  projlem18 9479  pjthlem1 9495  pjthlem5 9499  pjthlem6 9500  pjthlem7 9501  chdmm2i 9677  chj12i 9721  spanunsni 9778  qlaxr5i 9854  osumcor2i 9868  spansnji 9869  pjadjii 9896  pjinormii 9899  pjsslem 9902  pjpythi 9945  mayete3i 9951  mayete3OLDi 9952  mayetes3i 9953  hoadd12i 9983  honegneg 10012  ho2times 10025  hoaddsubi 10027  hosd1i 10028  hosd2i 10029  honpncani 10033  lnopeq0lem1 10209  lnopunilem1 10214  lnophmlem2 10221  lnfn0i 10250  nmopcoadji 10313  nmopcoadj2i 10314  kbass2 10330  kbass5 10333  pjclem3 10406  stadd3i 10456  mddmd2 10517  mdexchi 10543  cvexchlem 10576  atomli 10591  atordi 10593  atabs2i 10611  mdsymlem1 10612  1cat 11213  fsumltisumi 11886  csbrni 11895  trirni 11896  piececn 11955  txcnoprab 11981  phtpycolem2 12094  phtpyco 12098

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-sep 2777  ax-pow 2818  ax-pr 2855

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-v 1858  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-nul 2333  df-pw 2459  df-sn 2470  df-pr 2471  df-op 2474  df-uni 2570  df-br 2693  df-opab 2741  df-xp 3265  df-cnv 3267  df-dm 3269  df-rn 3270  df-res 3271  df-ima 3272  df-fv 3279  df-opr 4023

Copyright terms: Public domain