Theorem oveq2 6026

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 3863	. . 3 |- ( A = B -> <. C , A >. = <. C , B >. )
2	1	fveq2d 5643	. 2 |- ( A = B -> ( F ` <. C , A >. ) = ( F ` <. C , B >. ) )
3		df-ov 6021	. 2 |- ( C F A ) = ( F ` <. C , A >. )
4		df-ov 6021	. 2 |- ( C F B ) = ( F ` <. C , B >. )
5	2, 3, 4	3eqtr4g 2289	1 |- ( A = B -> ( C F A ) = ( C F B ) )

Syntax hints:   -> wi 4   = wceq 1397   <.cop 3672   ` cfv 5326  (class class class)co 6018

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6021

This theorem is referenced by:  oveq12  6027  oveq2i  6029  oveq2d  6034  ovanraleqv  6042  ovrspc2v  6044  oveqrspc2v  6045  rspceov  6061  fovcld  6126  ovmpos  6145  ov2gf  6146  ovi3  6159  caovclg  6175  caovcomg  6178  caovassg  6181  caovcang  6184  caovcan  6187  caovordig  6188  caovordg  6190  caovord  6194  caovdig  6197  caovdirg  6200  caovimo  6216  suppssov1  6232  off  6248  caofid0l  6262  caofid2  6265  caofdig  6269  omv  6623  oeiv  6624  oasuc  6632  oawordriexmid  6638  omsuc  6640  nna0r  6646  nnm0r  6647  nnacl  6648  nnmcl  6649  nnacom  6652  nnaass  6653  nndi  6654  nnmass  6655  nnmsucr  6656  nnmcom  6657  nnaordi  6676  nnaord  6677  nnmordi  6684  nnmord  6685  nnaordex  6696  nnawordex  6697  nnm00  6698  eroveu  6795  ecopovtrn  6801  ecopovtrng  6804  th3qlem2  6807  th3q  6809  ecovcom  6811  ecovicom  6812  ecovass  6813  ecoviass  6814  ecovdi  6815  ecovidi  6816  exmidpw2en  7104  acneq  7417  addcanpig  7554  mulcanpig  7555  addcmpblnq  7587  addclnq  7595  mulclnq  7596  recexnq  7610  recmulnqg  7611  ltanqg  7620  ltmnqg  7621  ltexnqq  7628  enq0ref  7653  enq0tr  7654  addcmpblnq0  7663  mulnnnq0  7670  addclnq0  7671  mulclnq0  7672  distrnq0  7679  mulcomnq0  7680  addassnq0  7682  nq02m  7685  prarloclem3  7717  genipv  7729  genpassl  7744  genpassu  7745  addlocpr  7756  distrlem1prl  7802  distrlem1pru  7803  1idprl  7810  1idpru  7811  ltexprlemell  7818  ltexprlemelu  7819  ltexpri  7833  lteupri  7837  ltaprlem  7838  recexprlem1ssl  7853  recexprlem1ssu  7854  recexpr  7858  cauappcvgprlemm  7865  cauappcvgprlemdisj  7871  cauappcvgprlemloc  7872  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  cauappcvgprlem1  7879  cauappcvgprlemlim  7881  cauappcvgpr  7882  mulcmpblnrlemg  7960  addclsr  7973  mulclsr  7974  ltasrg  7990  negexsr  7992  recexgt0sr  7993  mulgt0sr  7998  mulextsr1  8001  srpospr  8003  caucvgsrlemgt1  8015  map2psrprg  8025  axaddrcl  8085  axmulrcl  8087  axaddcom  8090  axrnegex  8099  axprecex  8100  axcnre  8101  axpre-ltadd  8106  axpre-mulgt0  8107  axpre-mulext  8108  rereceu  8109  recriota  8110  axcaucvglemres  8119  readdcan  8319  cnegexlem1  8354  cnegex  8357  addcan  8359  negeq  8372  subadd  8382  addid0  8552  ine0  8573  rimul  8765  cru  8782  apreim  8783  recexap  8833  mulcanapd  8841  receuap  8849  divmulap  8855  rerecapb  9023  cju  9141  nnaddcl  9163  nnmulcl  9164  nnsub  9182  nnnn0addcl  9432  zaddcllempos  9516  zaddcl  9519  zdiv  9568  deceq1  9615  deceq2  9616  uzaddcl  9820  zq  9860  qreccl  9876  cnref1o  9885  xaddnemnf  10092  xaddnepnf  10093  xaddcom  10096  xnn0xadd0  10102  xnegdi  10103  xaddass  10104  xlt2add  10115  xlesubadd  10118  xleaddadd  10122  fzsuc2  10314  fzrevral  10340  fzshftral  10343  2ffzeq  10376  exfzdc  10486  exbtwnzlemshrink  10508  rebtwn2zlemshrink  10513  modqval  10586  modqmuladd  10628  modqmuladdnn0  10630  frecuzrdgrrn  10670  frec2uzrdg  10671  frecuzrdgrcl  10672  frecuzrdgsuc  10676  frecuzrdgrclt  10677  frecuzrdgg  10678  frecuzrdgsuctlem  10685  frecfzennn  10688  uzsinds  10706  iseqvalcbv  10721  seq3val  10722  seqvalcd  10723  seqovcd  10729  seq3caopr3  10753  seq3caopr2  10755  seqcaopr2g  10756  seq3f1olemp  10777  seqf1og  10783  seq3id  10787  seq3homo  10789  seq3z  10790  seqhomog  10792  seqfeq4g  10793  seq3distr  10794  expp1  10808  expnegap0  10809  expcllem  10812  expcl2lemap  10813  m1expcl2  10823  expap0  10831  mulexp  10840  expadd  10843  expmul  10846  leexp2r  10855  leexp1a  10856  bernneq  10922  expnbnd  10925  modqexp  10928  nn0ltexp2  10971  expcan  10978  apexp1  10980  facdiv  11000  faclbnd3  11005  faclbnd6  11006  bcval  11011  bcpasc  11028  bccl  11029  fz1eqb  11052  omgadd  11065  hashunlem  11067  hashfzo  11086  hashfzp1  11088  iswrdinn0  11118  wrdnval  11144  eqwrd  11154  eqs1  11205  pfxeq  11277  ccatopth  11297  wrd2ind  11304  swrdccatin1  11306  swrdccatin2  11310  pfxccatin12lem2  11312  swrdccat3blem  11320  pfxccatid  11322  swrdccatin1d  11324  swrdccatin2d  11325  s2dmg  11371  shftfvalg  11379  shftfval  11382  cjth  11407  remim  11421  reim0b  11423  cjexp  11454  cnrecnv  11471  cvg1nlemcau  11545  cvg1nlemres  11546  recvguniq  11556  resqrexlemp1rp  11567  resqrexlemfp1  11570  resqrexlemlo  11574  resqrexlemgt0  11581  resqrexlemoverl  11582  resqrexlemglsq  11583  resqrexlemsqa  11585  resqrexlemex  11586  resqrex  11587  absexp  11640  recan  11670  climcn2  11870  subcn2  11872  summodc  11945  fsum3  11949  fsum3cvg3  11958  fsumrev  12005  fisum0diag2  12009  telfsumo  12028  fsumrelem  12033  binomlem  12045  binom  12046  binom1dif  12049  bcxmaslem1  12050  bcxmas  12051  isumshft  12052  divcnv  12059  arisum  12060  trireciplem  12062  expcnvap0  12064  expcnvre  12065  expcnv  12066  explecnv  12067  geosergap  12068  geolim  12073  geolim2  12074  geo2sum  12076  geo2lim  12078  geoisum  12079  geoisumr  12080  geoisum1  12081  geoisum1c  12082  cvgratnnlemsumlt  12090  cvgratz  12094  prodmodc  12140  fprodseq  12145  fprodcl2lem  12167  fprodfac  12177  fprodabs  12178  fprodrev  12181  eftvalcn  12219  efcvgfsum  12229  ege2le3  12233  efcj  12235  efaddlem  12236  efexp  12244  eftlub  12252  efgt1p2  12257  eflegeo  12263  sinval  12264  cosval  12265  demoivreALT  12336  divides  12351  dvdscmul  12380  dvds2ln  12386  dvdstr  12390  odd2np1lem  12434  odd2np1  12435  2tp1odd  12446  opeo  12459  omeo  12460  m1expe  12461  m1expo  12462  m1exp1  12463  divalglemnn  12480  divalglemeunn  12483  divalglemeuneg  12485  divalgmod  12489  ndvdssub  12492  bitsval  12505  bitsfzolem  12516  bitsinv1lem  12523  bitsinv1  12524  gcd0id  12551  bezoutlemnewy  12568  bezoutlema  12571  bezoutlemb  12572  bezoutlemex  12573  bezoutlemaz  12575  bezoutlembz  12576  gcdmultiple  12592  gcdmultiplez  12593  dvdsmulgcd  12597  rplpwr  12599  nn0seqcvgd  12614  dvdslcm  12642  lcmeq0  12644  lcmcl  12645  lcmneg  12647  lcmgcdlem  12650  lcmdvds  12652  lcmid  12653  lcmgcdeq  12656  coprmdvds  12665  mulgcddvds  12667  qredeq  12669  cncongr1  12676  cncongr2  12677  cncongrcoprm  12679  prmind2  12693  isprm6  12720  prmdvdsexp  12721  prmdvdsexpr  12723  sqrt2irr  12735  pw2dvdslemn  12738  pw2dvdseu  12741  oddpwdclemxy  12742  sqpweven  12748  2sqpwodd  12749  sqne2sq  12750  nn0gcdsq  12773  qden1elz  12778  phival  12786  dfphi2  12793  eulerthlemrprm  12802  eulerthlema  12803  prmdiv  12808  prmdiveq  12809  phisum  12814  odzval  12815  odzcllem  12816  odzdvds  12819  reumodprminv  12827  pythagtriplem3  12841  pythagtriplem18  12855  pythagtriplem19  12856  pclem0  12860  pclemub  12861  pclemdc  12862  pcprecl  12863  pcprendvds  12864  pcpremul  12867  pceulem  12868  pceu  12869  pczpre  12871  pcdiv  12876  pcqmul  12877  pcqcl  12880  pcexp  12883  pcxnn0cl  12884  pcxcl  12885  pcge0  12887  pcdvdsb  12894  pcneg  12899  pcabs  12900  pcgcd1  12902  pc2dvds  12904  pc11  12905  pcz  12906  pcprmpw2  12907  pcprmpw  12908  dvdsprmpweq  12909  dvdsprmpweqnn  12910  dvdsprmpweqle  12911  pcaddlem  12913  pcadd  12914  pcfac  12924  oddprmdvds  12928  prmpwdvds  12929  pockthi  12932  infpnlem2  12934  1arithlem1  12937  4sqlemffi  12970  4sqlem12  12976  2expltfac  13013  ennnfonelemnn0  13044  ennnfonelemr  13045  f1ovscpbl  13396  imasaddvallemg  13399  ercpbl  13415  mgm1  13454  mgmidmo  13456  mgmlrid  13463  lidrideqd  13465  lidrididd  13466  grpinvalem  13469  grpinva  13470  gsumfzval  13475  gsumval2  13481  isnsgrp  13490  sgrpass  13492  sgrp1  13495  mndinvmod  13529  imasmnd2  13536  mnd1  13539  mnd1id  13540  mhmpropd  13550  mhmlin  13551  insubm  13569  mhmima  13575  gsumwsubmcl  13580  gsumwmhm  13582  grpinvex  13594  grppropd  13601  dfgrp2  13611  grpidd2  13625  grpinvval  13627  grpinvid1  13636  grplrinv  13641  grpidinv2  13642  grpidinv  13643  grplcan  13646  grpidssd  13660  grpinvssd  13661  dfgrp3mlem  13682  dfgrp3m  13683  grplactcnv  13686  grp1  13690  imasgrp2  13698  mhmlem  13702  mulgnn0gsum  13716  mulginvcom  13735  mulgnn0ass  13746  mulgmodid  13749  issubg  13761  issubg2m  13777  issubg4m  13781  isnsg2  13791  nsgbi  13792  isnsg3  13795  elnmz  13796  nmzbi  13797  ghmlin  13836  ghmrn  13845  ghmnsgima  13856  conjghm  13864  conjnmz  13867  gsumfzconst  13929  rngdi  13955  rngdir  13956  srglz  14000  srgisid  14001  srglmhm  14008  ringid  14041  ringinvnz1ne0  14064  ringinvnzdiv  14065  ring1  14074  ringlghm  14076  imasring  14079  dvdsrtr  14117  lringuplu  14212  issubrng  14215  issubrng2  14226  issubrg  14237  issubrg2  14257  rrgeq0i  14280  rrgeq0  14281  unitrrg  14283  domneq0  14288  lmodlema  14308  islmodd  14309  rmodislmodlem  14366  rmodislmod  14367  lssclg  14380  lss1d  14399  rnglidlmcl  14496  quscrng  14549  cnfldexp  14593  gsumfzfsumlemm  14603  cnfldui  14605  expghmap  14623  zrhval  14633  zrhvalg  14634  znunit  14675  txdis1cn  15004  cnmptcom  15024  psmettri2  15054  isxmet2d  15074  xmeteq0  15085  xmettri2  15087  elblps  15116  elbl  15117  blssps  15153  blss  15154  ssblex  15157  blin2  15158  metss2  15224  comet  15225  bdmopn  15230  txmetcnp  15244  blssioo  15279  divcnap  15291  mpomulcn  15292  expcn  15295  cncfval  15298  cncfi  15304  mulc1cncf  15315  cdivcncfap  15330  mulcncf  15334  expcncf  15335  cnopnap  15337  ellimc3apf  15386  cnlimci  15399  limccnpcntop  15401  limccnp2lem  15402  reldvg  15405  eldvap  15408  dvexp  15437  dvexp2  15438  dvrecap  15439  elplyr  15466  elplyd  15467  ply1termlem  15468  plymullem1  15474  plyadd  15477  plymul  15478  plycoeid3  15483  plycolemc  15484  plyco  15485  plycj  15487  dvply1  15491  dvply2g  15492  sin0pilem2  15508  rpcxpmul2  15639  relogbcxpbap  15691  logbgcd1irr  15693  2irrexpq  15702  2irrexpqap  15704  dvdsppwf1o  15715  mpodvdsmulf1o  15716  fsumdvdsmul  15717  sgmppw  15718  1sgmprm  15720  perfect  15727  lgsneg  15755  lgsdilem  15758  lgsdir  15766  lgsdilem2  15767  lgsdi  15768  lgsne0  15769  lgsdirnn0  15778  lgsdinn0  15779  gausslemma2dlem4  15795  lgseisenlem2  15802  lgseisenlem3  15803  lgseisenlem4  15804  lgsquadlem1  15808  lgsquadlem2  15809  lgsquad2lem2  15813  2lgs  15835  2sqlem6  15851  2sqlem8  15854  2sqlem9  15855  2sqlem10  15856  wlkeq  16207  wlkl1loop  16211  uspgr2wlkeq  16218  upgr2wlkdc  16230  clwwlknonmpo  16281  trilpolemclim  16643  trilpolemcl  16644  trilpolemisumle  16645  trilpolemeq1  16647  trilpolemlt1  16648  trilpo  16650  trirec0  16651  redcwlpo  16662  nconstwlpolemgt0  16671  nconstwlpo  16673  neapmkv  16675