Theorem oveq1i 5928

Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)

Hypothesis

Ref	Expression
oveq1i.1	|- A = B

Assertion

Ref	Expression
oveq1i	|- ( A F C ) = ( B F C )

Proof of Theorem oveq1i

Step	Hyp	Ref	Expression
1		oveq1i.1	. 2 |- A = B
2		oveq1 5925	. 2 |- ( A = B -> ( A F C ) = ( B F C ) )
3	1, 2	ax-mp 5	1 |- ( A F C ) = ( B F C )

Syntax hints:   = wceq 1364  (class class class)co 5918

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-v 2762  df-un 3157  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-iota 5215  df-fv 5262  df-ov 5921

This theorem is referenced by:  caov12  6107  map1  6866  exmidpw2en  6968  halfnqq  7470  prarloclem5  7560  m1m1sr  7821  caucvgsrlemfv  7851  caucvgsr  7862  pitonnlem1  7905  axi2m1  7935  axcnre  7941  axcaucvg  7960  mvrraddi  8236  mvlladdi  8237  negsubdi  8275  mul02  8406  mulneg1  8414  mulreim  8623  recextlem1  8670  recdivap  8737  2p2e4  9109  2times  9110  3p2e5  9123  3p3e6  9124  4p2e6  9125  4p3e7  9126  4p4e8  9127  5p2e7  9128  5p3e8  9129  5p4e9  9130  6p2e8  9131  6p3e9  9132  7p2e9  9133  1mhlfehlf  9200  8th4div3  9201  halfpm6th  9202  nneoor  9419  9p1e10  9450  dfdec10  9451  num0h  9459  numsuc  9461  dec10p  9490  numma  9491  nummac  9492  numma2c  9493  numadd  9494  numaddc  9495  nummul2c  9497  decaddci  9508  decsubi  9510  decmul1  9511  5p5e10  9518  6p4e10  9519  7p3e10  9522  8p2e10  9527  decbin0  9587  decbin2  9588  elfzp1b  10163  elfzm1b  10164  fz01or  10177  fz1ssfz0  10183  fz0to4untppr  10190  qbtwnrelemcalc  10324  fldiv4p1lem1div2  10374  1tonninf  10512  mulexpzap  10650  expaddzap  10654  sq4e2t8  10708  cu2  10709  i3  10712  iexpcyc  10715  binom2i  10719  binom3  10728  3dec  10785  faclbnd  10812  bcm1k  10831  bcp1nk  10833  bcpasc  10837  hashp1i  10881  hashxp  10897  imre  10995  crim  11002  remullem  11015  resqrexlemfp1  11153  resqrexlemover  11154  resqrexlemcalc1  11158  resqrexlemnm  11162  absexpzap  11224  absimle  11228  amgm2  11262  maxabslemlub  11351  fsumconst  11597  modfsummod  11601  binomlem  11626  binom11  11629  arisum  11641  arisum2  11642  georeclim  11656  geo2sum  11657  mertenslemi1  11678  mertenslem2  11679  mertensabs  11680  prodfrecap  11689  fprodm1s  11744  fprodp1s  11745  fprodrec  11772  fprodmodd  11784  efzval  11826  resinval  11858  recosval  11859  efi4p  11860  tan0  11874  efival  11875  cosadd  11880  cos2tsin  11894  ef01bndlem  11899  cos1bnd  11902  cos2bnd  11903  absefib  11914  efieq1re  11915  demoivreALT  11917  eirraplem  11920  3dvdsdec  12006  3dvds2dec  12007  odd2np1  12014  nn0o1gt2  12046  nn0o  12048  flodddiv4  12075  algrp1  12184  3lcm2e6woprm  12224  nn0gcdsq  12338  phiprmpw  12360  prmdiv  12373  prmdiveq  12374  pythagtriplem1  12403  pythagtriplem12  12413  pythagtriplem14  12415  pockthi  12496  infpnlem1  12497  4sqlem12  12540  4sqlem13m  12541  4sqlem19  12547  subsubm  13055  mulg2  13201  subsubg  13267  unitsubm  13615  subsubrng  13710  subsubrg  13741  lsslss  13877  expghmap  14095  cnmpt1res  14464  rerestcntop  14718  dvfvalap  14835  dvcnp2cntop  14848  dveflem  14872  plyun0  14882  reeff1oleme  14907  sin0pilem1  14916  sinhalfpilem  14926  cospi  14935  eulerid  14937  cos2pi  14939  ef2kpi  14941  sinhalfpip  14955  sinhalfpim  14956  coshalfpip  14957  coshalfpim  14958  sincosq3sgn  14963  sincosq4sgn  14964  cosq23lt0  14968  tangtx  14973  sincos4thpi  14975  sincos6thpi  14977  cosq34lt1  14985  rplogb1  15080  2logb9irr  15103  sqrt2cxp2logb9e3  15107  2logb9irrap  15109  binom4  15111  lgsdir2lem1  15144  lgsdir2lem2  15145  lgsdir2lem4  15147  lgsdir2lem5  15148  lgsne0  15154  1lgs  15159  gausslemma2dlem0e  15169  gausslemma2dlem0f  15170  gausslemma2dlem3  15179  gausslemma2d  15185  lgseisenlem1  15186  lgseisenlem2  15187  lgseisenlem3  15188  lgseisenlem4  15189  lgseisen  15190  lgsquadlem1  15191  m1lgs  15192  2lgsoddprmlem3a  15195  2lgsoddprmlem3b  15196  2lgsoddprmlem3c  15197  2lgsoddprmlem3d  15198  ex-fl  15217  ex-exp  15219  ex-bc  15221  012of  15486  2o01f  15487  qdencn  15517  isomninnlem  15520  iswomninnlem  15539  ismkvnnlem  15542