Theorem oveq2 5834

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

Assertion

Ref	Expression
oveq2	|- ( A = B -> ( C F A ) = ( C F B ) )

Proof of Theorem oveq2

Step	Hyp	Ref	Expression
1		opeq2 3744	. . 3 |- ( A = B -> <. C , A >. = <. C , B >. )
2	1	fveq2d 5474	. 2 |- ( A = B -> ( F ` <. C , A >. ) = ( F ` <. C , B >. ) )
3		df-ov 5829	. 2 |- ( C F A ) = ( F ` <. C , A >. )
4		df-ov 5829	. 2 |- ( C F B ) = ( F ` <. C , B >. )
5	2, 3, 4	3eqtr4g 2215	1 |- ( A = B -> ( C F A ) = ( C F B ) )

Syntax hints:   -> wi 4   = wceq 1335   <.cop 3564   ` cfv 5172  (class class class)co 5826

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-rex 2441  df-v 2714  df-un 3106  df-sn 3567  df-pr 3568  df-op 3570  df-uni 3775  df-br 3968  df-iota 5137  df-fv 5180  df-ov 5829

This theorem is referenced by:  oveq12  5835  oveq2i  5837  oveq2d  5842  ovanraleqv  5850  rspceov  5865  fovcl  5928  ovmpos  5946  ov2gf  5947  ovi3  5959  caovclg  5975  caovcomg  5978  caovassg  5981  caovcang  5984  caovcan  5987  caovordig  5988  caovordg  5990  caovord  5994  caovdig  5997  caovdirg  6000  caovimo  6016  grprinvlem  6017  grprinvd  6018  suppssov1  6031  off  6046  omv  6404  oeiv  6405  oasuc  6413  oawordriexmid  6419  omsuc  6421  nna0r  6427  nnm0r  6428  nnacl  6429  nnmcl  6430  nnacom  6433  nnaass  6434  nndi  6435  nnmass  6436  nnmsucr  6437  nnmcom  6438  nnaordi  6457  nnaord  6458  nnmordi  6465  nnmord  6466  nnaordex  6476  nnawordex  6477  nnm00  6478  eroveu  6573  ecopovtrn  6579  ecopovtrng  6582  th3qlem2  6585  th3q  6587  ecovcom  6589  ecovicom  6590  ecovass  6591  ecoviass  6592  ecovdi  6593  ecovidi  6594  addcanpig  7256  mulcanpig  7257  addcmpblnq  7289  addclnq  7297  mulclnq  7298  recexnq  7312  recmulnqg  7313  ltanqg  7322  ltmnqg  7323  ltexnqq  7330  enq0ref  7355  enq0tr  7356  addcmpblnq0  7365  mulnnnq0  7372  addclnq0  7373  mulclnq0  7374  distrnq0  7381  mulcomnq0  7382  addassnq0  7384  nq02m  7387  prarloclem3  7419  genipv  7431  genpassl  7446  genpassu  7447  addlocpr  7458  distrlem1prl  7504  distrlem1pru  7505  1idprl  7512  1idpru  7513  ltexprlemell  7520  ltexprlemelu  7521  ltexpri  7535  lteupri  7539  ltaprlem  7540  recexprlem1ssl  7555  recexprlem1ssu  7556  recexpr  7560  cauappcvgprlemm  7567  cauappcvgprlemdisj  7573  cauappcvgprlemloc  7574  cauappcvgprlemladdru  7578  cauappcvgprlemladdrl  7579  cauappcvgprlem1  7581  cauappcvgprlemlim  7583  cauappcvgpr  7584  mulcmpblnrlemg  7662  addclsr  7675  mulclsr  7676  ltasrg  7692  negexsr  7694  recexgt0sr  7695  mulgt0sr  7700  mulextsr1  7703  srpospr  7705  caucvgsrlemgt1  7717  map2psrprg  7727  axaddrcl  7787  axmulrcl  7789  axaddcom  7792  axrnegex  7801  axprecex  7802  axcnre  7803  axpre-ltadd  7808  axpre-mulgt0  7809  axpre-mulext  7810  rereceu  7811  recriota  7812  axcaucvglemres  7821  readdcan  8019  cnegexlem1  8054  cnegex  8057  addcan  8059  negeq  8072  subadd  8082  addid0  8252  ine0  8273  rimul  8464  cru  8481  apreim  8482  recexap  8531  mulcanapd  8539  receuap  8547  divmulap  8552  cju  8837  nnaddcl  8858  nnmulcl  8859  nnsub  8877  nnnn0addcl  9125  zaddcllempos  9209  zaddcl  9212  zdiv  9257  deceq1  9304  deceq2  9305  uzaddcl  9502  zq  9541  qreccl  9557  cnref1o  9565  xaddnemnf  9767  xaddnepnf  9768  xaddcom  9771  xnn0xadd0  9777  xnegdi  9778  xaddass  9779  xlt2add  9790  xlesubadd  9793  xleaddadd  9797  fzsuc2  9987  fzrevral  10013  fzshftral  10016  2ffzeq  10049  exfzdc  10148  exbtwnzlemshrink  10157  rebtwn2zlemshrink  10162  modqval  10232  modqmuladd  10274  modqmuladdnn0  10276  frecuzrdgrrn  10316  frec2uzrdg  10317  frecuzrdgrcl  10318  frecuzrdgsuc  10322  frecuzrdgrclt  10323  frecuzrdgg  10324  frecuzrdgsuctlem  10331  frecfzennn  10334  uzsinds  10350  iseqvalcbv  10365  seq3val  10366  seqvalcd  10367  seqovcd  10371  seq3caopr3  10389  seq3caopr2  10390  seq3f1olemp  10410  seq3id  10416  seq3homo  10418  seq3z  10419  seq3distr  10421  expp1  10435  expnegap0  10436  expcllem  10439  expcl2lemap  10440  m1expcl2  10450  expap0  10458  mulexp  10467  expadd  10470  expmul  10473  leexp2r  10482  leexp1a  10483  bernneq  10547  expnbnd  10550  modqexp  10553  nn0ltexp2  10595  expcan  10601  apexp1  10603  facdiv  10623  faclbnd3  10628  faclbnd6  10629  bcval  10634  bcpasc  10651  bccl  10652  fz1eqb  10676  omgadd  10687  hashunlem  10689  hashfzo  10707  hashfzp1  10709  shftfvalg  10729  shftfval  10732  cjth  10757  remim  10771  reim0b  10773  cjexp  10804  cnrecnv  10821  cvg1nlemcau  10895  cvg1nlemres  10896  recvguniq  10906  resqrexlemp1rp  10917  resqrexlemfp1  10920  resqrexlemlo  10924  resqrexlemgt0  10931  resqrexlemoverl  10932  resqrexlemglsq  10933  resqrexlemsqa  10935  resqrexlemex  10936  resqrex  10937  absexp  10990  recan  11020  climcn2  11217  subcn2  11219  summodc  11291  fsum3  11295  fsum3cvg3  11304  fsumrev  11351  fisum0diag2  11355  telfsumo  11374  fsumrelem  11379  binomlem  11391  binom  11392  binom1dif  11395  bcxmaslem1  11396  bcxmas  11397  isumshft  11398  divcnv  11405  arisum  11406  trireciplem  11408  expcnvap0  11410  expcnvre  11411  expcnv  11412  explecnv  11413  geosergap  11414  geolim  11419  geolim2  11420  geo2sum  11422  geo2lim  11424  geoisum  11425  geoisumr  11426  geoisum1  11427  geoisum1c  11428  cvgratnnlemsumlt  11436  cvgratz  11440  prodmodc  11486  fprodseq  11491  fprodcl2lem  11513  fprodfac  11523  fprodabs  11524  fprodrev  11527  eftvalcn  11565  efcvgfsum  11575  ege2le3  11579  efcj  11581  efaddlem  11582  efexp  11590  eftlub  11598  efgt1p2  11603  eflegeo  11609  sinval  11610  cosval  11611  demoivreALT  11681  divides  11696  dvdscmul  11725  dvds2ln  11731  dvdstr  11735  odd2np1lem  11775  odd2np1  11776  2tp1odd  11787  opeo  11800  omeo  11801  m1expe  11802  m1expo  11803  m1exp1  11804  divalglemnn  11821  divalglemeunn  11824  divalglemeuneg  11826  divalgmod  11830  ndvdssub  11833  gcd0id  11878  bezoutlemnewy  11895  bezoutlema  11898  bezoutlemb  11899  bezoutlemex  11900  bezoutlemaz  11902  bezoutlembz  11903  gcdmultiple  11919  gcdmultiplez  11920  dvdsmulgcd  11924  rplpwr  11926  nn0seqcvgd  11933  dvdslcm  11961  lcmeq0  11963  lcmcl  11964  lcmneg  11966  lcmgcdlem  11969  lcmdvds  11971  lcmid  11972  lcmgcdeq  11975  coprmdvds  11984  mulgcddvds  11986  qredeq  11988  cncongr1  11995  cncongr2  11996  cncongrcoprm  11998  prmind2  12012  isprm6  12037  prmdvdsexp  12038  prmdvdsexpr  12040  sqrt2irr  12052  pw2dvdslemn  12055  pw2dvdseu  12058  oddpwdclemxy  12059  sqpweven  12065  2sqpwodd  12066  sqne2sq  12067  nn0gcdsq  12090  qden1elz  12095  phival  12103  dfphi2  12110  eulerthlemrprm  12119  eulerthlema  12120  prmdiv  12125  prmdiveq  12126  phisum  12130  odzval  12131  odzcllem  12132  odzdvds  12135  reumodprminv  12143  pythagtriplem3  12157  pythagtriplem18  12171  pythagtriplem19  12172  pclem0  12176  pclemub  12177  pclemdc  12178  pcprecl  12179  pcprendvds  12180  pcpremul  12183  pceulem  12184  pceu  12185  pczpre  12187  ennnfonelemnn0  12221  ennnfonelemr  12222  txdis1cn  12748  cnmptcom  12768  psmettri2  12798  isxmet2d  12818  xmeteq0  12829  xmettri2  12831  elblps  12860  elbl  12861  blssps  12897  blss  12898  ssblex  12901  blin2  12902  metss2  12968  comet  12969  bdmopn  12974  txmetcnp  12988  blssioo  13015  divcnap  13025  cncfval  13029  cncfi  13035  mulc1cncf  13046  cdivcncfap  13057  mulcncf  13061  expcncf  13062  cnopnap  13064  ellimc3apf  13099  cnlimci  13112  limccnpcntop  13114  limccnp2lem  13115  reldvg  13118  eldvap  13121  dvexp  13145  dvexp2  13146  dvrecap  13147  sin0pilem2  13173  relogbcxpbap  13353  logbgcd1irr  13355  2irrexpq  13364  2irrexpqap  13366  trilpolemclim  13678  trilpolemcl  13679  trilpolemisumle  13680  trilpolemeq1  13682  trilpolemlt1  13683  trilpo  13685  trirec0  13686  redcwlpo  13697  nconstwlpolemgt0  13705  nconstwlpo  13707  neapmkv  13709