Theorem oveq2 5849

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 3758	. . 3 |- ( A = B -> <. C , A >. = <. C , B >. )
2	1	fveq2d 5489	. 2 |- ( A = B -> ( F ` <. C , A >. ) = ( F ` <. C , B >. ) )
3		df-ov 5844	. 2 |- ( C F A ) = ( F ` <. C , A >. )
4		df-ov 5844	. 2 |- ( C F B ) = ( F ` <. C , B >. )
5	2, 3, 4	3eqtr4g 2223	1 |- ( A = B -> ( C F A ) = ( C F B ) )

Syntax hints:   -> wi 4   = wceq 1343   <.cop 3578   ` cfv 5187  (class class class)co 5841

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-rex 2449  df-v 2727  df-un 3119  df-sn 3581  df-pr 3582  df-op 3584  df-uni 3789  df-br 3982  df-iota 5152  df-fv 5195  df-ov 5844

This theorem is referenced by:  oveq12  5850  oveq2i  5852  oveq2d  5857  ovanraleqv  5865  rspceov  5880  fovcl  5943  ovmpos  5961  ov2gf  5962  ovi3  5974  caovclg  5990  caovcomg  5993  caovassg  5996  caovcang  5999  caovcan  6002  caovordig  6003  caovordg  6005  caovord  6009  caovdig  6012  caovdirg  6015  caovimo  6031  grprinvlem  6032  grprinvd  6033  suppssov1  6046  off  6061  omv  6419  oeiv  6420  oasuc  6428  oawordriexmid  6434  omsuc  6436  nna0r  6442  nnm0r  6443  nnacl  6444  nnmcl  6445  nnacom  6448  nnaass  6449  nndi  6450  nnmass  6451  nnmsucr  6452  nnmcom  6453  nnaordi  6472  nnaord  6473  nnmordi  6480  nnmord  6481  nnaordex  6491  nnawordex  6492  nnm00  6493  eroveu  6588  ecopovtrn  6594  ecopovtrng  6597  th3qlem2  6600  th3q  6602  ecovcom  6604  ecovicom  6605  ecovass  6606  ecoviass  6607  ecovdi  6608  ecovidi  6609  addcanpig  7271  mulcanpig  7272  addcmpblnq  7304  addclnq  7312  mulclnq  7313  recexnq  7327  recmulnqg  7328  ltanqg  7337  ltmnqg  7338  ltexnqq  7345  enq0ref  7370  enq0tr  7371  addcmpblnq0  7380  mulnnnq0  7387  addclnq0  7388  mulclnq0  7389  distrnq0  7396  mulcomnq0  7397  addassnq0  7399  nq02m  7402  prarloclem3  7434  genipv  7446  genpassl  7461  genpassu  7462  addlocpr  7473  distrlem1prl  7519  distrlem1pru  7520  1idprl  7527  1idpru  7528  ltexprlemell  7535  ltexprlemelu  7536  ltexpri  7550  lteupri  7554  ltaprlem  7555  recexprlem1ssl  7570  recexprlem1ssu  7571  recexpr  7575  cauappcvgprlemm  7582  cauappcvgprlemdisj  7588  cauappcvgprlemloc  7589  cauappcvgprlemladdru  7593  cauappcvgprlemladdrl  7594  cauappcvgprlem1  7596  cauappcvgprlemlim  7598  cauappcvgpr  7599  mulcmpblnrlemg  7677  addclsr  7690  mulclsr  7691  ltasrg  7707  negexsr  7709  recexgt0sr  7710  mulgt0sr  7715  mulextsr1  7718  srpospr  7720  caucvgsrlemgt1  7732  map2psrprg  7742  axaddrcl  7802  axmulrcl  7804  axaddcom  7807  axrnegex  7816  axprecex  7817  axcnre  7818  axpre-ltadd  7823  axpre-mulgt0  7824  axpre-mulext  7825  rereceu  7826  recriota  7827  axcaucvglemres  7836  readdcan  8034  cnegexlem1  8069  cnegex  8072  addcan  8074  negeq  8087  subadd  8097  addid0  8267  ine0  8288  rimul  8479  cru  8496  apreim  8497  recexap  8546  mulcanapd  8554  receuap  8562  divmulap  8567  cju  8852  nnaddcl  8873  nnmulcl  8874  nnsub  8892  nnnn0addcl  9140  zaddcllempos  9224  zaddcl  9227  zdiv  9275  deceq1  9322  deceq2  9323  uzaddcl  9520  zq  9560  qreccl  9576  cnref1o  9584  xaddnemnf  9789  xaddnepnf  9790  xaddcom  9793  xnn0xadd0  9799  xnegdi  9800  xaddass  9801  xlt2add  9812  xlesubadd  9815  xleaddadd  9819  fzsuc2  10010  fzrevral  10036  fzshftral  10039  2ffzeq  10072  exfzdc  10171  exbtwnzlemshrink  10180  rebtwn2zlemshrink  10185  modqval  10255  modqmuladd  10297  modqmuladdnn0  10299  frecuzrdgrrn  10339  frec2uzrdg  10340  frecuzrdgrcl  10341  frecuzrdgsuc  10345  frecuzrdgrclt  10346  frecuzrdgg  10347  frecuzrdgsuctlem  10354  frecfzennn  10357  uzsinds  10373  iseqvalcbv  10388  seq3val  10389  seqvalcd  10390  seqovcd  10394  seq3caopr3  10412  seq3caopr2  10413  seq3f1olemp  10433  seq3id  10439  seq3homo  10441  seq3z  10442  seq3distr  10444  expp1  10458  expnegap0  10459  expcllem  10462  expcl2lemap  10463  m1expcl2  10473  expap0  10481  mulexp  10490  expadd  10493  expmul  10496  leexp2r  10505  leexp1a  10506  bernneq  10571  expnbnd  10574  modqexp  10577  nn0ltexp2  10619  expcan  10625  apexp1  10627  facdiv  10647  faclbnd3  10652  faclbnd6  10653  bcval  10658  bcpasc  10675  bccl  10676  fz1eqb  10700  omgadd  10711  hashunlem  10713  hashfzo  10731  hashfzp1  10733  shftfvalg  10756  shftfval  10759  cjth  10784  remim  10798  reim0b  10800  cjexp  10831  cnrecnv  10848  cvg1nlemcau  10922  cvg1nlemres  10923  recvguniq  10933  resqrexlemp1rp  10944  resqrexlemfp1  10947  resqrexlemlo  10951  resqrexlemgt0  10958  resqrexlemoverl  10959  resqrexlemglsq  10960  resqrexlemsqa  10962  resqrexlemex  10963  resqrex  10964  absexp  11017  recan  11047  climcn2  11246  subcn2  11248  summodc  11320  fsum3  11324  fsum3cvg3  11333  fsumrev  11380  fisum0diag2  11384  telfsumo  11403  fsumrelem  11408  binomlem  11420  binom  11421  binom1dif  11424  bcxmaslem1  11425  bcxmas  11426  isumshft  11427  divcnv  11434  arisum  11435  trireciplem  11437  expcnvap0  11439  expcnvre  11440  expcnv  11441  explecnv  11442  geosergap  11443  geolim  11448  geolim2  11449  geo2sum  11451  geo2lim  11453  geoisum  11454  geoisumr  11455  geoisum1  11456  geoisum1c  11457  cvgratnnlemsumlt  11465  cvgratz  11469  prodmodc  11515  fprodseq  11520  fprodcl2lem  11542  fprodfac  11552  fprodabs  11553  fprodrev  11556  eftvalcn  11594  efcvgfsum  11604  ege2le3  11608  efcj  11610  efaddlem  11611  efexp  11619  eftlub  11627  efgt1p2  11632  eflegeo  11638  sinval  11639  cosval  11640  demoivreALT  11710  divides  11725  dvdscmul  11754  dvds2ln  11760  dvdstr  11764  odd2np1lem  11805  odd2np1  11806  2tp1odd  11817  opeo  11830  omeo  11831  m1expe  11832  m1expo  11833  m1exp1  11834  divalglemnn  11851  divalglemeunn  11854  divalglemeuneg  11856  divalgmod  11860  ndvdssub  11863  gcd0id  11908  bezoutlemnewy  11925  bezoutlema  11928  bezoutlemb  11929  bezoutlemex  11930  bezoutlemaz  11932  bezoutlembz  11933  gcdmultiple  11949  gcdmultiplez  11950  dvdsmulgcd  11954  rplpwr  11956  nn0seqcvgd  11969  dvdslcm  11997  lcmeq0  11999  lcmcl  12000  lcmneg  12002  lcmgcdlem  12005  lcmdvds  12007  lcmid  12008  lcmgcdeq  12011  coprmdvds  12020  mulgcddvds  12022  qredeq  12024  cncongr1  12031  cncongr2  12032  cncongrcoprm  12034  prmind2  12048  isprm6  12075  prmdvdsexp  12076  prmdvdsexpr  12078  sqrt2irr  12090  pw2dvdslemn  12093  pw2dvdseu  12096  oddpwdclemxy  12097  sqpweven  12103  2sqpwodd  12104  sqne2sq  12105  nn0gcdsq  12128  qden1elz  12133  phival  12141  dfphi2  12148  eulerthlemrprm  12157  eulerthlema  12158  prmdiv  12163  prmdiveq  12164  phisum  12168  odzval  12169  odzcllem  12170  odzdvds  12173  reumodprminv  12181  pythagtriplem3  12195  pythagtriplem18  12209  pythagtriplem19  12210  pclem0  12214  pclemub  12215  pclemdc  12216  pcprecl  12217  pcprendvds  12218  pcpremul  12221  pceulem  12222  pceu  12223  pczpre  12225  pcdiv  12230  pcqmul  12231  pcqcl  12234  pcexp  12237  pcxnn0cl  12238  pcxcl  12239  pcge0  12240  pcdvdsb  12247  pcneg  12252  pcabs  12253  pcgcd1  12255  pc2dvds  12257  pc11  12258  pcz  12259  pcprmpw2  12260  pcprmpw  12261  dvdsprmpweq  12262  dvdsprmpweqnn  12263  dvdsprmpweqle  12264  pcaddlem  12266  pcadd  12267  pcfac  12276  oddprmdvds  12280  prmpwdvds  12281  pockthi  12284  infpnlem2  12286  1arithlem1  12289  ennnfonelemnn0  12351  ennnfonelemr  12352  txdis1cn  12878  cnmptcom  12898  psmettri2  12928  isxmet2d  12948  xmeteq0  12959  xmettri2  12961  elblps  12990  elbl  12991  blssps  13027  blss  13028  ssblex  13031  blin2  13032  metss2  13098  comet  13099  bdmopn  13104  txmetcnp  13118  blssioo  13145  divcnap  13155  cncfval  13159  cncfi  13165  mulc1cncf  13176  cdivcncfap  13187  mulcncf  13191  expcncf  13192  cnopnap  13194  ellimc3apf  13229  cnlimci  13242  limccnpcntop  13244  limccnp2lem  13245  reldvg  13248  eldvap  13251  dvexp  13275  dvexp2  13276  dvrecap  13277  sin0pilem2  13303  relogbcxpbap  13483  logbgcd1irr  13485  2irrexpq  13494  2irrexpqap  13496  lgsneg  13525  lgsdilem  13528  lgsdir  13536  lgsdilem2  13537  lgsdi  13538  lgsne0  13539  lgsdirnn0  13548  lgsdinn0  13549  2sqlem6  13556  2sqlem8  13559  2sqlem9  13560  2sqlem10  13561  trilpolemclim  13875  trilpolemcl  13876  trilpolemisumle  13877  trilpolemeq1  13879  trilpolemlt1  13880  trilpo  13882  trirec0  13883  redcwlpo  13894  nconstwlpolemgt0  13902  nconstwlpo  13904  neapmkv  13906