Theorem opreq1i 3962

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

Syntax hints:   = wceq 954  (class class class)co 3954

This theorem is referenced by:  opreq12i 3964  caopr12 4053  caopr411 4057  map1 4417  cdaassen 4910  distrpq 5047  ltapq 5056  ltmpq 5057  ltexpq 5060  halfpq 5062  addclprlem2 5099  prlem934a 5117  m1m1sr 5182  recexsrlem 5192  axi2m1 5265  axcnre 5266  negneg 5370  mul12 5403  mulneg1 5425  ltneg 5585  ixi 5662  recextlem1 5663  div23 5719  divcan4 5723  divcan4z 5725  recrec 5733  rec11i 5741  divmul13 5751  recdivt 5754  divdiv23 5757  prodgt0lem 5782  nnsub 5911  2p2e4 5956  2times 5958  3p2e5 5962  3p3e6 5963  4p2e6 5964  4p3e7 5965  4p4e8 5966  5p2e7 5967  5p3e8 5968  5p4e9 5969  5p5e10 5970  6p2e8 5971  6p3e9 5972  6p4e10 5973  7p2e9 5974  7p3e10 5975  8p2e10 5976  8th4div3 5986  halfpm6th 5987  nneo 6152  uzindOLD 6164  om2uzsuc 6241  recexpt 6534  sqreci 6557  cu2 6579  binom2 6583  binom2aOLD 6584  discrlem1 6594  nnesq 6600  nn0opthlem1 6602  nn0opth2 6605  sqrlem11 6621  sqrlem16 6626  i3 6671  crulem 6674  crmul 6679  crrecz 6680  rimul 6683  cjdiv 6834  abslem2i 6853  faclbnd 6890  bcpasc2 6913  fsump1f 6957  binomlem1 7012  binomlem2 7013  binomlem4 7015  binomlem6 7017  iserzshft 7088  isumnn0nn 7150  fnsmntlem 7168  fnsmnt 7169  geoser 7177  geolimilem 7178  geolim1i 7181  georeclim 7183  geoisumr 7186  cvgratlem1ALT 7190  cvgratlem3ALT 7192  efseq0ex 7261  efaddlem5 7292  efaddlem6 7293  efaddlem16 7303  efaddlem20 7307  efaddlem22 7309  efnn0valt 7323  ef1tllem 7331  eirrlem3 7340  abspef01tlub 7344  efm1lim 7359  efm1legeo 7365  efcnlem2 7368  resinvalt 7383  recosvalt 7384  efi4pt 7385  efivalt 7397  sinadd 7401  cosadd 7402  cos2tOLD 7414  sin01bndlem1 7417  sin01bndlem2 7418  cos01bndlem2 7420  cos1bnd 7424  cos2bnd 7425  demoivre 7434  acdc3lem 7436  acdc2lem2 7439  acdc5lem2 7442  acdclem 7444  infpnlem1 7457  ruclem1 7461  ruclem2 7462  ruclem3 7463  ruclem15 7475  fsumcnlem 7939  vc2 8126  vc0 8140  vcm 8142  vcnegneg 8145  nvnncan 8235  nvm1 8244  nvpi 8246  nvmtri 8251  nvge0 8254  ipval2lem1 8298  ipval2 8304  ipval3 8306  ipid 8310  ip0i 8428  ip1ilem 8429  ip2i 8431  ipdirilem 8432  ipasslem10 8443  siilem1 8455  siii 8457  minveclem19 8507  minveclem27 8515  minveclem35 8523  minveclem38 8526  sinhalfpilem 8617  cospi 8620  eulerid 8621  cos2pi 8623  sinperlem1 8624  sinhalfpip 8635  sinhalfpim 8636  coshalfpip 8637  coshalfpim 8638  sincosq3sgn 8642  sincosq4sgn 8643  sincos4thpi 8646  sincos6thpi 8647  pilog 8707  hvsubidt 8834  hvaddsubvalt 8841  hvmul2neg 8854  hvsubass 8861  hvadd12 8863  hv2timest 8867  hvnegdi 8868  hvaddcan 8871  hi01t 8901  hisubcom 8909  normlem0 8914  normlem1 8915  normlem3 8917  normlem9 8923  bcseq 8925  normsq 8938  norm-ii 8943  normsub 8947  norm3dif 8953  norm3adif 8954  normpar2 8962  polid2 8963  polid 8964  occllem1 9112  projlem3 9127  projlem4 9128  projlem18 9142  pjthlem1 9157  pjthlem5 9161  pjthlem6 9162  pjthlem7 9163  chdmm2 9339  chj12 9383  spanunsn 9442  qlaxr5 9516  osumcor2 9530  spansnj 9531  pjadj 9558  pjinorm 9561  pjsslem 9564  pjpyth 9607  mayete3 9613  hoadd12 9643  honegnegt 9672  ho2timest 9685  hoaddsub 9687  hosd1 9688  hosd2 9689  honpncan 9693  lnopeq0lem1 9868  lnopunilem1 9873  lnophmlem2 9880  lnfn0 9909  nmopcoadj 9972  nmopcoadj2 9973  kbass2t 9988  kbass5t 9991  pjclem3 10063  stadd3 10113  mddmd 10173  mdexch 10199  cvexchlem 10232  atoml 10246  atord 10248  atabs2 10266  mdsymlem1 10267  1cat 10572

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698  ax-pow 2737  ax-pr 2774

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409  df-op 2412  df-uni 2499  df-br 2615  df-opab 2662  df-xp 3179  df-cnv 3181  df-dm 3183  df-rn 3184  df-res 3185  df-ima 3186  df-fv 3193  df-opr 3956

Copyright terms: Public domain