Theorem opreq1i 4892

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

Syntax hints:   = wceq 1298  (class class class)co 4884

This theorem is referenced by:  opreq12iOLD 4895  caopr12 4994  caopr411 4998  map1 5489  cdaassen 6080  distrpq 6219  ltapq 6228  ltmpq 6229  ltexpq 6232  halfpq 6234  addclprlem2 6271  prlem934a 6289  m1m1sr 6354  recexsrlem 6364  axi2m1 6438  axcnre 6439  negnegiOLD 6550  mul12iOLD 6586  mulneg1i 6608  ltnegi 6783  ixiOLD 6873  recextlem1 6874  div23i 6931  divcan4i 6935  divcan4zi 6937  recreci 6945  rec11ii 6953  divmul13i 6964  recdiv 6967  divdiv23i 6970  prodgt0lem 6996  nnsubi 7140  2p2e4 7185  2timesi 7187  3p2e5 7191  3p3e6 7192  4p2e6 7193  4p3e7 7194  4p4e8 7195  5p2e7 7196  5p3e8 7197  5p4e9 7198  5p5e10 7199  6p2e8 7200  6p3e9 7201  6p4e10 7202  7p2e9 7203  7p3e10 7204  8p2e10 7205  8th4div3 7217  halfpm6th 7218  nneoi 7409  uzindOLD 7420  quoremz 7492  quoremnn0 7494  om2uzsuci 7707  exprec 7837  exprecOLD 7838  sqrecii 7864  cu2 7885  binom2i 7890  binom2aiOLD 7891  discrlem1 7906  nnesqi 7912  nn0opthlem1 7914  nn0opth2i 7917  sqrlem11 7933  sqrlem16 7938  i3 7983  crulem 7986  crmuli 7990  crreczi 7991  rimul 7994  imre 8023  cjdivi 8140  abslem2i 8160  faclbnd 8197  bcpasc2i 8219  fsump1fi 8271  binomlem1 8326  binomlem2 8327  binomlem4 8329  binomlem6 8331  iserzshfti 8404  isumnn0nn 8468  arisumilem 8486  arisumi 8487  geoseri 8496  geolimilem 8497  geolim1i 8500  georeclim 8502  geoisumr 8505  cvgratlem1ALT 8509  cvgratlem3ALT 8511  efseq0ex 8573  efaddlem5 8604  efaddlem6 8605  efaddlem16 8615  efaddlem20 8619  efaddlem22 8621  efnn0val 8635  ef1tllem 8643  eirrlem3 8653  abspef01tlubi 8660  efm1limi 8676  efm1legeoi 8682  efcnlem2 8685  resinval 8698  recosval 8699  efi4p 8700  efival 8712  sinaddi 8716  cosaddi 8717  cos2tsin 8729  cos2OLD 8730  sin01bndlem1 8733  sin01bndlem2 8734  cos01bndlem2 8736  cos1bnd 8740  cos2bnd 8741  absefib 8750  efieq1re 8751  demoivre 8752  acdc3lem 8754  acdc2lem2 8758  acdc5lem2 8761  acdclem 8763  infpnlem1 8775  ruclem1 8779  ruclem2 8780  ruclem3 8781  ruclem15 8793  fsumcnlem 9267  vc2 9506  vc0 9520  vcm 9522  vcnegneg 9525  nvnncan 9615  nvm1 9624  nvpi 9626  nvmtri 9631  nvge0 9634  ipval2lem1 9690  ipval2 9696  ipval3 9698  ipid 9702  ip0i 9825  ip1ilem 9826  ip2i 9828  ipdirilem 9829  ipasslem10 9840  siilem1 9852  siii 9854  minveclem19 9908  minveclem27 9916  minveclem35 9924  minveclem38 9927  sinhalfpilem 10028  cospi 10031  eulerid 10032  cos2pi 10034  sinperlem1 10035  sinhalfpip 10048  sinhalfpim 10049  coshalfpip 10050  coshalfpim 10051  sincosq3sgn 10055  sincosq4sgn 10056  sincos4thpi 10060  sincos6thpi 10061  sineq0re 10067  pilog 10122  hvsubid 10527  hvaddsubval 10534  hvmul2negi 10547  hvsubassi 10554  hvadd12i 10556  hv2times 10560  hvnegdii 10561  hvaddcani 10564  hi01 10595  hisubcomi 10603  normlem0 10608  normlem1 10609  normlem3 10611  normlem9 10617  bcseqi 10619  normsqi 10632  norm-ii.i 10637  normsubi 10641  norm3difi 10647  norm3adifii 10648  normpar2i 10656  polid2i 10657  polidi 10658  occllem1 10806  projlem3 10821  projlem4 10822  projlem18 10836  pjthlem1 10852  pjthlem5 10856  pjthlem6 10857  pjthlem7 10858  chdmm2i 11034  chj12i 11078  spanunsni 11135  qlaxr5i 11211  osumcor2i 11225  spansnji 11226  pjadjii 11253  pjinormii 11256  pjsslem 11259  pjpythi 11302  mayete3i 11308  mayete3OLDi 11309  mayetes3i 11310  hoadd12i 11340  honegneg 11369  ho2times 11382  hoaddsubi 11384  hosd1i 11385  hosd2i 11386  honpncani 11390  lnopeq0lem1 11567  lnopunilem1 11572  lnophmlem2 11579  lnfn0i 11608  nmopcoadji 11671  nmopcoadj2i 11672  kbass2 11688  kbass5 11691  opsqrlem1 11711  opsqrlem5 11715  opsqrlem6 11716  pjclem3 11770  stadd3i 11820  mddmd2 11881  mdexchi 11907  cvexchlem 11940  atomli 11954  atordi 11956  atabs2i 11974  mdsymlem1 11975  elfzp1b 13605  elfzm1b 13606  divalglem2 13698  divalglem9 13704  gcdaddmlem 13734  algrp1 13742  eucalgcvga 13754  mulgcdlem5 13760  3timesi 14523  fprodp1fi 14680  vecax3 14798  cntrsetlem 14999  1cat 15106  fdc 15812  fsumltisumi 15823  csbrni 15832  trirni 15833  piececn 15894  txcnoprab 15911  phtpycolem2 16052  phtpyco 16056  reparphtlem2 16064  reparpht 16065  pcoval2 16075  pco1 16078  pcohtpylem2 16081  pcohtpylem3 16082  pcohtpy 16083  pcoass 16085  pcorevlem 16086  pcorev 16087  pmod2i 17310

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-xp 4000  df-cnv 4002  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fv 4014  df-opr 4886

Copyright terms: Public domain