Theorem opreq1i 3971

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 3968	. 2 |- (A = B -> (AFC) = (BFC))
3	1, 2	ax-mp 7	1 |- (AFC) = (BFC)

Syntax hints:   = wceq 956  (class class class)co 3963

This theorem is referenced by:  opreq12i 3973  caopr12 4061  caopr411 4065  map1 4430  cdaassen 4930  distrpq 5067  ltapq 5076  ltmpq 5077  ltexpq 5080  halfpq 5082  addclprlem2 5119  prlem934a 5137  m1m1sr 5202  recexsrlem 5212  axi2m1 5285  axcnre 5286  negneg 5390  mul12 5423  mulneg1 5445  ltneg 5603  ixi 5681  recextlem1 5682  div23 5748  divcan4 5753  divcan4z 5755  recrec 5769  rec11i 5777  divmul13 5787  recdivt 5790  divdiv23 5793  prodgt0lem 5818  nnsub 5956  2p2e4 6001  2times 6003  3p2e5 6007  3p3e6 6008  4p2e6 6009  4p3e7 6010  4p4e8 6011  5p2e7 6012  5p3e8 6013  5p4e9 6014  5p5e10 6015  6p2e8 6016  6p3e9 6017  6p4e10 6018  7p2e9 6019  7p3e10 6020  8p2e10 6021  8th4div3 6031  halfpm6th 6032  nneo 6197  uzindOLD 6208  quoremz 6251  om2uzsuc 6296  recexpt 6595  sqreci 6619  cu2 6640  binom2 6644  binom2aOLD 6645  discrlem1 6656  nnesq 6662  nn0opthlem1 6664  nn0opth2 6667  sqrlem11 6683  sqrlem16 6688  i3 6733  crulem 6736  crmul 6740  crrecz 6741  rimul 6744  imret 6773  cjdiv 6888  abslem2i 6908  faclbnd 6945  bcpasc2 6967  fsump1f 7011  binomlem1 7066  binomlem2 7067  binomlem4 7069  binomlem6 7071  iserzshft 7144  isumnn0nn 7207  fnsmntlem 7225  fnsmnt 7226  geoser 7234  geolimilem 7235  geolim1i 7238  georeclim 7240  geoisumr 7243  cvgratlem1ALT 7247  cvgratlem3ALT 7249  efseq0ex 7311  efaddlem5 7342  efaddlem6 7343  efaddlem16 7353  efaddlem20 7357  efaddlem22 7359  efnn0valt 7373  ef1tllem 7381  eirrlem3 7391  abspef01tlub 7395  efm1lim 7411  efm1legeo 7417  efcnlem2 7420  resinvalt 7433  recosvalt 7434  efi4pt 7435  efivalt 7447  sinadd 7451  cosadd 7452  cos2tOLD 7464  sin01bndlem1 7467  sin01bndlem2 7468  cos01bndlem2 7470  cos1bnd 7474  cos2bnd 7475  demoivre 7484  acdc3lem 7486  acdc2lem2 7489  acdc5lem2 7492  acdclem 7494  infpnlem1 7506  ruclem1 7510  ruclem2 7511  ruclem3 7512  ruclem15 7524  fsumcnlem 7989  vc2 8174  vc0 8188  vcm 8190  vcnegneg 8193  nvnncan 8283  nvm1 8292  nvpi 8294  nvmtri 8299  nvge0 8302  ipval2lem1 8351  ipval2 8357  ipval3 8359  ipid 8363  ip0i 8484  ip1ilem 8485  ip2i 8487  ipdirilem 8488  ipasslem10 8499  siilem1 8511  siii 8513  minveclem19 8563  minveclem27 8571  minveclem35 8579  minveclem38 8582  sinhalfpilem 8679  cospi 8682  eulerid 8683  cos2pi 8685  sinperlem1 8686  sinhalfpip 8699  sinhalfpim 8700  coshalfpip 8701  coshalfpim 8702  sincosq3sgn 8706  sincosq4sgn 8707  sincos4thpi 8710  sincos6thpi 8711  pilog 8768  hvsubidt 8895  hvaddsubvalt 8902  hvmul2neg 8915  hvsubass 8922  hvadd12 8924  hv2timest 8928  hvnegdi 8929  hvaddcan 8932  hi01t 8962  hisubcom 8970  normlem0 8975  normlem1 8976  normlem3 8978  normlem9 8984  bcseq 8986  normsq 8999  norm-ii 9004  normsub 9008  norm3dif 9014  norm3adif 9015  normpar2 9023  polid2 9024  polid 9025  occllem1 9173  projlem3 9188  projlem4 9189  projlem18 9203  pjthlem1 9219  pjthlem5 9223  pjthlem6 9224  pjthlem7 9225  chdmm2 9401  chj12 9445  spanunsn 9502  qlaxr5 9576  osumcor2 9590  spansnj 9591  pjadj 9618  pjinorm 9621  pjsslem 9624  pjpyth 9667  mayete3 9673  hoadd12 9703  honegnegt 9732  ho2timest 9745  hoaddsub 9747  hosd1 9748  hosd2 9749  honpncan 9753  lnopeq0lem1 9930  lnopunilem1 9935  lnophmlem2 9942  lnfn0 9971  nmopcoadj 10034  nmopcoadj2 10035  kbass2t 10050  kbass5t 10053  pjclem3 10125  stadd3 10175  mddmd 10236  mdexch 10262  cvexchlem 10295  atoml 10309  atord 10311  atabs2 10329  mdsymlem1 10330  1cat 10692

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703  ax-pow 2742  ax-pr 2779

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413  df-op 2416  df-uni 2504  df-br 2620  df-opab 2667  df-xp 3184  df-cnv 3186  df-dm 3188  df-rn 3189  df-res 3190  df-ima 3191  df-fv 3198  df-opr 3965

Copyright terms: Public domain