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 997  (class class class)co 4021

This theorem is referenced by:  opreq12i 4031  caopr12 4119  caopr411 4123  map1 4491  cdaassen 4995  distrpq 5132  ltapq 5141  ltmpq 5142  ltexpq 5145  halfpq 5147  addclprlem2 5184  prlem934a 5202  m1m1sr 5267  recexsrlem 5277  axi2m1 5350  axcnre 5351  negnegi 5455  mul12i 5488  mulneg1i 5510  ltnegi 5668  ixi 5746  recextlem1 5747  div23i 5811  divcan4i 5816  divcan4zi 5818  recreci 5826  rec11ii 5835  divmul13i 5845  recdiv 5848  divdiv23i 5851  prodgt0lem 5876  nnsubi 6017  2p2e4 6062  2timesi 6064  3p2e5 6068  3p3e6 6069  4p2e6 6070  4p3e7 6071  4p4e8 6072  5p2e7 6073  5p3e8 6074  5p4e9 6075  5p5e10 6076  6p2e8 6077  6p3e9 6078  6p4e10 6079  7p2e9 6080  7p3e10 6081  8p2e10 6082  8th4div3 6092  halfpm6th 6093  nneoi 6282  uzindOLD 6293  quoremz 6363  quoremnn0 6365  om2uzsuci 6554  recexp 6684  sqrecii 6708  cu2 6729  binom2i 6733  binom2aiOLD 6734  discrlem1 6746  nnesqi 6752  nn0opthlem1 6754  nn0opth2i 6757  sqrlem11 6773  sqrlem16 6778  i3 6823  crulem 6826  crmuli 6830  crreczi 6831  rimul 6834  imre 6863  cjdivi 6978  abslem2i 6998  faclbnd 7035  bcpasc2i 7057  fsump1fi 7101  binomlem1 7156  binomlem2 7157  binomlem4 7159  binomlem6 7161  iserzshfti 7234  isumnn0nn 7297  arisumilem 7315  arisumi 7316  geoseri 7324  geolimilem 7325  geolim1i 7328  georeclim 7330  geoisumr 7333  cvgratlem1ALT 7337  cvgratlem3ALT 7339  efseq0ex 7401  efaddlem5 7432  efaddlem6 7433  efaddlem16 7443  efaddlem20 7447  efaddlem22 7449  efnn0val 7463  ef1tllem 7471  eirrlem3 7481  abspef01tlubi 7486  efm1limi 7502  efm1legeoi 7508  efcnlem2 7511  resinval 7524  recosval 7525  efi4p 7526  efival 7538  sinaddi 7542  cosaddi 7543  cos2tsin 7555  cos2OLD 7556  sin01bndlem1 7559  sin01bndlem2 7560  cos01bndlem2 7562  cos1bnd 7566  cos2bnd 7567  demoivre 7576  acdc3lem 7578  acdc2lem2 7581  acdc5lem2 7584  acdclem 7586  infpnlem1 7598  ruclem1 7602  ruclem2 7603  ruclem3 7604  ruclem15 7616  fsumcnlem 8074  vc2 8258  vc0 8272  vcm 8274  vcnegneg 8277  nvnncan 8367  nvm1 8376  nvpi 8378  nvmtri 8383  nvge0 8386  ipval2lem1 8435  ipval2 8441  ipval3 8443  ipid 8447  ip0i 8568  ip1ilem 8569  ip2i 8571  ipdirilem 8572  ipasslem10 8583  siilem1 8595  siii 8597  minveclem19 8647  minveclem27 8655  minveclem35 8663  minveclem38 8666  sinhalfpilem 8762  cospi 8765  eulerid 8766  cos2pi 8768  sinperlem1 8769  sinhalfpip 8782  sinhalfpim 8783  coshalfpip 8784  coshalfpim 8785  sincosq3sgn 8789  sincosq4sgn 8790  sincos4thpi 8793  sincos6thpi 8794  pilog 8851  hvsubid 8978  hvaddsubval 8985  hvmul2negi 8998  hvsubassi 9005  hvadd12i 9007  hv2times 9011  hvnegdii 9012  hvaddcani 9015  hi01 9045  hisubcomi 9053  normlem0 9058  normlem1 9059  normlem3 9061  normlem9 9067  bcseqi 9069  normsqi 9082  norm-ii.i 9087  normsubi 9091  norm3difi 9097  norm3adifii 9098  normpar2i 9106  polid2i 9107  polidi 9108  occllem1 9256  projlem3 9271  projlem4 9272  projlem18 9286  pjthlem1 9302  pjthlem5 9306  pjthlem6 9307  pjthlem7 9308  chdmm2i 9484  chj12i 9528  spanunsni 9585  qlaxr5i 9659  osumcor2i 9673  spansnji 9674  pjadjii 9701  pjinormii 9704  pjsslem 9707  pjpythi 9750  mayete3i 9756  hoadd12i 9786  honegneg 9815  ho2times 9828  hoaddsubi 9830  hosd1i 9831  hosd2i 9832  honpncani 9836  lnopeq0lem1 10013  lnopunilem1 10018  lnophmlem2 10025  lnfn0i 10054  nmopcoadji 10117  nmopcoadj2i 10118  kbass2 10133  kbass5 10136  pjclem3 10209  stadd3i 10259  mddmd2 10320  mdexchi 10346  cvexchlem 10379  atomli 10393  atordi 10395  atabs2i 10413  mdsymlem1 10414  1cat 10774

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-sep 2758  ax-pow 2798  ax-pr 2835

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-v 1859  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-nul 2332  df-pw 2454  df-sn 2464  df-pr 2465  df-op 2468  df-uni 2558  df-br 2675  df-opab 2722  df-xp 3241  df-cnv 3243  df-dm 3245  df-rn 3246  df-res 3247  df-ima 3248  df-fv 3255  df-opr 4023

Copyright terms: Public domain