Theorem oveq2 5782

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 3706	. . 3 |- ( A = B -> <. C , A >. = <. C , B >. )
2	1	fveq2d 5425	. 2 |- ( A = B -> ( F ` <. C , A >. ) = ( F ` <. C , B >. ) )
3		df-ov 5777	. 2 |- ( C F A ) = ( F ` <. C , A >. )
4		df-ov 5777	. 2 |- ( C F B ) = ( F ` <. C , B >. )
5	2, 3, 4	3eqtr4g 2197	1 |- ( A = B -> ( C F A ) = ( C F B ) )

Syntax hints:   -> wi 4   = wceq 1331   <.cop 3530   ` cfv 5123  (class class class)co 5774

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-rex 2422  df-v 2688  df-un 3075  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-br 3930  df-iota 5088  df-fv 5131  df-ov 5777

This theorem is referenced by:  oveq12  5783  oveq2i  5785  oveq2d  5790  ovanraleqv  5798  rspceov  5813  fovcl  5876  ovmpos  5894  ov2gf  5895  ovi3  5907  caovclg  5923  caovcomg  5926  caovassg  5929  caovcang  5932  caovcan  5935  caovordig  5936  caovordg  5938  caovord  5942  caovdig  5945  caovdirg  5948  caovimo  5964  grprinvlem  5965  grprinvd  5966  suppssov1  5979  off  5994  omv  6351  oeiv  6352  oasuc  6360  oawordriexmid  6366  omsuc  6368  nna0r  6374  nnm0r  6375  nnacl  6376  nnmcl  6377  nnacom  6380  nnaass  6381  nndi  6382  nnmass  6383  nnmsucr  6384  nnmcom  6385  nnaordi  6404  nnaord  6405  nnmordi  6412  nnmord  6413  nnaordex  6423  nnawordex  6424  nnm00  6425  eroveu  6520  ecopovtrn  6526  ecopovtrng  6529  th3qlem2  6532  th3q  6534  ecovcom  6536  ecovicom  6537  ecovass  6538  ecoviass  6539  ecovdi  6540  ecovidi  6541  addcanpig  7142  mulcanpig  7143  addcmpblnq  7175  addclnq  7183  mulclnq  7184  recexnq  7198  recmulnqg  7199  ltanqg  7208  ltmnqg  7209  ltexnqq  7216  enq0ref  7241  enq0tr  7242  addcmpblnq0  7251  mulnnnq0  7258  addclnq0  7259  mulclnq0  7260  distrnq0  7267  mulcomnq0  7268  addassnq0  7270  nq02m  7273  prarloclem3  7305  genipv  7317  genpassl  7332  genpassu  7333  addlocpr  7344  distrlem1prl  7390  distrlem1pru  7391  1idprl  7398  1idpru  7399  ltexprlemell  7406  ltexprlemelu  7407  ltexpri  7421  lteupri  7425  ltaprlem  7426  recexprlem1ssl  7441  recexprlem1ssu  7442  recexpr  7446  cauappcvgprlemm  7453  cauappcvgprlemdisj  7459  cauappcvgprlemloc  7460  cauappcvgprlemladdru  7464  cauappcvgprlemladdrl  7465  cauappcvgprlem1  7467  cauappcvgprlemlim  7469  cauappcvgpr  7470  mulcmpblnrlemg  7548  addclsr  7561  mulclsr  7562  ltasrg  7578  negexsr  7580  recexgt0sr  7581  mulgt0sr  7586  mulextsr1  7589  srpospr  7591  caucvgsrlemgt1  7603  map2psrprg  7613  axaddrcl  7673  axmulrcl  7675  axaddcom  7678  axrnegex  7687  axprecex  7688  axcnre  7689  axpre-ltadd  7694  axpre-mulgt0  7695  axpre-mulext  7696  rereceu  7697  recriota  7698  axcaucvglemres  7707  readdcan  7902  cnegexlem1  7937  cnegex  7940  addcan  7942  negeq  7955  subadd  7965  addid0  8135  ine0  8156  rimul  8347  cru  8364  apreim  8365  recexap  8414  mulcanapd  8422  receuap  8430  divmulap  8435  cju  8719  nnaddcl  8740  nnmulcl  8741  nnsub  8759  nnnn0addcl  9007  zaddcllempos  9091  zaddcl  9094  zdiv  9139  deceq1  9186  deceq2  9187  uzaddcl  9381  zq  9418  qreccl  9434  cnref1o  9440  xaddnemnf  9640  xaddnepnf  9641  xaddcom  9644  xnn0xadd0  9650  xnegdi  9651  xaddass  9652  xlt2add  9663  xlesubadd  9666  xleaddadd  9670  fzsuc2  9859  fzrevral  9885  fzshftral  9888  2ffzeq  9918  exfzdc  10017  exbtwnzlemshrink  10026  rebtwn2zlemshrink  10031  modqval  10097  modqmuladd  10139  modqmuladdnn0  10141  frecuzrdgrrn  10181  frec2uzrdg  10182  frecuzrdgrcl  10183  frecuzrdgsuc  10187  frecuzrdgrclt  10188  frecuzrdgg  10189  frecuzrdgsuctlem  10196  frecfzennn  10199  uzsinds  10215  iseqvalcbv  10230  seq3val  10231  seqvalcd  10232  seqovcd  10236  seq3caopr3  10254  seq3caopr2  10255  seq3f1olemp  10275  seq3id  10281  seq3homo  10283  seq3z  10284  seq3distr  10286  expp1  10300  expnegap0  10301  expcllem  10304  expcl2lemap  10305  m1expcl2  10315  expap0  10323  mulexp  10332  expadd  10335  expmul  10338  leexp2r  10347  leexp1a  10348  bernneq  10412  expnbnd  10415  expcan  10463  facdiv  10484  faclbnd3  10489  faclbnd6  10490  bcval  10495  bcpasc  10512  bccl  10513  fz1eqb  10537  omgadd  10548  hashunlem  10550  hashfzo  10568  hashfzp1  10570  shftfvalg  10590  shftfval  10593  cjth  10618  remim  10632  reim0b  10634  cjexp  10665  cnrecnv  10682  cvg1nlemcau  10756  cvg1nlemres  10757  recvguniq  10767  resqrexlemp1rp  10778  resqrexlemfp1  10781  resqrexlemlo  10785  resqrexlemgt0  10792  resqrexlemoverl  10793  resqrexlemglsq  10794  resqrexlemsqa  10796  resqrexlemex  10797  resqrex  10798  absexp  10851  recan  10881  climcn2  11078  subcn2  11080  summodc  11152  fsum3  11156  fsum3cvg3  11165  fsumrev  11212  fisum0diag2  11216  telfsumo  11235  fsumrelem  11240  binomlem  11252  binom  11253  binom1dif  11256  bcxmaslem1  11257  bcxmas  11258  isumshft  11259  divcnv  11266  arisum  11267  trireciplem  11269  expcnvap0  11271  expcnvre  11272  expcnv  11273  explecnv  11274  geosergap  11275  geolim  11280  geolim2  11281  geo2sum  11283  geo2lim  11285  geoisum  11286  geoisumr  11287  geoisum1  11288  geoisum1c  11289  cvgratnnlemsumlt  11297  cvgratz  11301  prodmodc  11347  eftvalcn  11363  efcvgfsum  11373  ege2le3  11377  efcj  11379  efaddlem  11380  efexp  11388  eftlub  11396  efgt1p2  11401  eflegeo  11408  sinval  11409  cosval  11410  demoivreALT  11480  divides  11495  dvdscmul  11520  dvds2ln  11526  dvdstr  11530  odd2np1lem  11569  odd2np1  11570  2tp1odd  11581  opeo  11594  omeo  11595  m1expe  11596  m1expo  11597  m1exp1  11598  divalglemnn  11615  divalglemeunn  11618  divalglemeuneg  11620  divalgmod  11624  ndvdssub  11627  gcd0id  11667  bezoutlemnewy  11684  bezoutlema  11687  bezoutlemb  11688  bezoutlemex  11689  bezoutlemaz  11691  bezoutlembz  11692  gcdmultiple  11708  gcdmultiplez  11709  dvdsmulgcd  11713  rplpwr  11715  nn0seqcvgd  11722  dvdslcm  11750  lcmeq0  11752  lcmcl  11753  lcmneg  11755  lcmgcdlem  11758  lcmdvds  11760  lcmid  11761  lcmgcdeq  11764  coprmdvds  11773  mulgcddvds  11775  qredeq  11777  cncongr1  11784  cncongr2  11785  cncongrcoprm  11787  prmind2  11801  isprm6  11825  prmdvdsexp  11826  prmdvdsexpr  11828  sqrt2irr  11840  pw2dvdslemn  11843  pw2dvdseu  11846  oddpwdclemxy  11847  sqpweven  11853  2sqpwodd  11854  sqne2sq  11855  nn0gcdsq  11878  qden1elz  11883  phival  11889  dfphi2  11896  ennnfonelemnn0  11935  ennnfonelemr  11936  txdis1cn  12447  cnmptcom  12467  psmettri2  12497  isxmet2d  12517  xmeteq0  12528  xmettri2  12530  elblps  12559  elbl  12560  blssps  12596  blss  12597  ssblex  12600  blin2  12601  metss2  12667  comet  12668  bdmopn  12673  txmetcnp  12687  blssioo  12714  divcnap  12724  cncfval  12728  cncfi  12734  mulc1cncf  12745  cdivcncfap  12756  mulcncf  12760  expcncf  12761  cnopnap  12763  ellimc3apf  12798  cnlimci  12811  limccnpcntop  12813  limccnp2lem  12814  reldvg  12817  eldvap  12820  dvexp  12844  dvexp2  12845  dvrecap  12846  sin0pilem2  12863  trilpolemclim  13229  trilpolemcl  13230  trilpolemisumle  13231  trilpolemeq1  13233  trilpolemlt1  13234  trilpo  13236