Theorem oveq2 5540

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 3571	. . 3 |- ( A = B -> <. C , A >. = <. C , B >. )
2	1	fveq2d 5202	. 2 |- ( A = B -> ( F ` <. C , A >. ) = ( F ` <. C , B >. ) )
3		df-ov 5535	. 2 |- ( C F A ) = ( F ` <. C , A >. )
4		df-ov 5535	. 2 |- ( C F B ) = ( F ` <. C , B >. )
5	2, 3, 4	3eqtr4g 2138	1 |- ( A = B -> ( C F A ) = ( C F B ) )

Syntax hints:   -> wi 4   = wceq 1284   <.cop 3401   ` cfv 4922  (class class class)co 5532

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-3an 921  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-rex 2354  df-v 2603  df-un 2977  df-sn 3404  df-pr 3405  df-op 3407  df-uni 3602  df-br 3786  df-iota 4887  df-fv 4930  df-ov 5535

This theorem is referenced by:  oveq12  5541  oveq2i  5543  oveq2d  5548  rspceov  5567  fovcl  5626  ovmpt2s  5644  ov2gf  5645  ovi3  5657  caovclg  5673  caovcomg  5676  caovassg  5679  caovcang  5682  caovcan  5685  caovordig  5686  caovordg  5688  caovord  5692  caovdig  5695  caovdirg  5698  caovimo  5714  grprinvlem  5715  grprinvd  5716  suppssov1  5729  off  5744  omv  6058  oeiv  6059  oasuc  6067  omsuc  6074  nna0r  6080  nnm0r  6081  nnacl  6082  nnmcl  6083  nnacom  6086  nnaass  6087  nndi  6088  nnmass  6089  nnmsucr  6090  nnmcom  6091  nnaordi  6104  nnaord  6105  nnmordi  6112  nnmord  6113  nnaordex  6123  nnawordex  6124  nnm00  6125  eroveu  6220  ecopovtrn  6226  ecopovtrng  6229  th3qlem2  6232  th3q  6234  ecovcom  6236  ecovicom  6237  ecovass  6238  ecoviass  6239  ecovdi  6240  ecovidi  6241  addcanpig  6524  mulcanpig  6525  addcmpblnq  6557  addclnq  6565  mulclnq  6566  recexnq  6580  recmulnqg  6581  ltanqg  6590  ltmnqg  6591  ltexnqq  6598  enq0ref  6623  enq0tr  6624  addcmpblnq0  6633  mulnnnq0  6640  addclnq0  6641  mulclnq0  6642  distrnq0  6649  mulcomnq0  6650  addassnq0  6652  nq02m  6655  prarloclem3  6687  genipv  6699  genpassl  6714  genpassu  6715  addlocpr  6726  distrlem1prl  6772  distrlem1pru  6773  1idprl  6780  1idpru  6781  ltexprlemell  6788  ltexprlemelu  6789  ltexpri  6803  lteupri  6807  ltaprlem  6808  recexprlem1ssl  6823  recexprlem1ssu  6824  recexpr  6828  cauappcvgprlemm  6835  cauappcvgprlemdisj  6841  cauappcvgprlemloc  6842  cauappcvgprlemladdru  6846  cauappcvgprlemladdrl  6847  cauappcvgprlem1  6849  cauappcvgprlemlim  6851  cauappcvgpr  6852  mulcmpblnrlemg  6917  addclsr  6930  mulclsr  6931  ltasrg  6947  negexsr  6949  recexgt0sr  6950  mulgt0sr  6954  mulextsr1  6957  srpospr  6959  caucvgsrlemgt1  6971  axaddrcl  7033  axmulrcl  7035  axaddcom  7036  axrnegex  7045  axprecex  7046  axcnre  7047  axpre-ltadd  7052  axpre-mulgt0  7053  axpre-mulext  7054  rereceu  7055  recriota  7056  axcaucvglemres  7065  readdcan  7248  cnegexlem1  7283  cnegex  7286  addcan  7288  negeq  7301  subadd  7311  addid0  7477  ine0  7498  rimul  7685  cru  7702  apreim  7703  recexap  7743  mulcanapd  7751  receuap  7759  divmulap  7763  cju  8038  nnaddcl  8059  nnmulcl  8060  nnsub  8077  nnnn0addcl  8318  zaddcllempos  8388  zaddcl  8391  zdiv  8435  deceq1  8481  deceq2  8482  uzaddcl  8674  zq  8711  qreccl  8727  cnref1o  8733  fzsuc2  9096  fzrevral  9122  fzshftral  9125  2ffzeq  9151  exfzdc  9249  qbtwnzlemshrink  9258  rebtwn2zlemshrink  9262  modqval  9326  modqmuladd  9368  modqmuladdnn0  9370  frecuzrdgrrn  9410  frec2uzrdg  9411  frecuzrdgsuc  9417  frecfzennn  9419  uzsinds  9428  iseqcaopr3  9460  iseqcaopr2  9461  iseqid  9467  iseqhomo  9468  iseqz  9469  iseqdistr  9470  expp1  9483  expnegap0  9484  expcllem  9487  expcl2lemap  9488  m1expcl2  9498  expap0  9506  mulexp  9515  expadd  9518  expmul  9521  leexp2r  9530  leexp1a  9531  bernneq  9593  expnbnd  9596  expcan  9644  facdiv  9665  faclbnd3  9670  faclbnd6  9671  bcval  9676  bcpasc  9693  bccl  9694  shftfvalg  9706  shftfval  9709  cjth  9733  remim  9747  reim0b  9749  cjexp  9780  cnrecnv  9797  cvg1nlemcau  9870  cvg1nlemres  9871  recvguniq  9881  resqrexlemp1rp  9892  resqrexlemfp1  9895  resqrexlemlo  9899  resqrexlemgt0  9906  resqrexlemoverl  9907  resqrexlemglsq  9908  resqrexlemsqa  9910  resqrexlemex  9911  resqrex  9912  absexp  9965  recan  9995  climcn2  10148  subcn2  10150  divides  10197  dvdscmul  10222  dvds2ln  10228  dvdstr  10232  odd2np1lem  10271  odd2np1  10272  2tp1odd  10284  opeo  10297  omeo  10298  m1expe  10299  m1expo  10300  m1exp1  10301  divalglemnn  10318  divalglemeunn  10321  divalglemeuneg  10323  divalgmod  10327  ndvdssub  10330  gcd0id  10370  bezoutlemnewy  10385  bezoutlema  10388  bezoutlemb  10389  bezoutlemex  10390  bezoutlemaz  10392  bezoutlembz  10393  gcdmultiple  10409  gcdmultiplez  10410  dvdsmulgcd  10414  rplpwr  10416  nn0seqcvgd  10423  dvdslcm  10451  lcmeq0  10453  lcmcl  10454  lcmneg  10456  lcmgcdlem  10459  lcmdvds  10461  lcmid  10462  lcmgcdeq  10465  coprmdvds  10474  mulgcddvds  10476  qredeq  10478  cncongr1  10485  cncongr2  10486  cncongrcoprm  10488  prmind2  10502  isprm6  10526  prmdvdsexp  10527  prmdvdsexpr  10529  sqrt2irr  10541  pw2dvdslemn  10543  pw2dvdseu  10546  oddpwdclemxy  10547  sqpweven  10553  2sqpwodd  10554  sqne2sq  10555