Theorem oveq2 6093

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 3905	. . 3 |- ( A = B -> <. C , A >. = <. C , B >. )
2	1	fveq2d 5699	. 2 |- ( A = B -> ( F ` <. C , A >. ) = ( F ` <. C , B >. ) )
3		df-ov 6088	. 2 |- ( C F A ) = ( F ` <. C , A >. )
4		df-ov 6088	. 2 |- ( C F B ) = ( F ` <. C , B >. )
5	2, 3, 4	3eqtr4g 2296	1 |- ( A = B -> ( C F A ) = ( C F B ) )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   <.cop 3712   ` cfv 5377  (class class class)co 6085

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385  df-ov 6088

This theorem is used by:  oveq12  6094  oveq2i  6096  oveq2d  6101  ovanraleqv  6109  ovrspc2v  6111  oveqrspc2v  6112  rspceov  6128  fovcld  6193  ovmpos  6212  ov2gf  6213  ovi3  6226  caovclg  6242  caovcomg  6245  caovassg  6248  caovcang  6251  caovcan  6254  caovordig  6255  caovordg  6257  caovord  6261  caovdig  6264  caovdirg  6267  caovimo  6283  suppssov1  6299  off  6315  caofid0l  6329  caofid2  6332  caofdig  6336  suppofss1dcl  6504  suppofss2dcl  6505  omv  6728  oeiv  6729  oasuc  6737  oawordriexmid  6743  omsuc  6745  nna0r  6751  nnm0r  6752  nnacl  6753  nnmcl  6754  nnacom  6757  nnaass  6758  nndi  6759  nnmass  6760  nnmsucr  6761  nnmcom  6762  nnaordi  6781  nnaord  6782  nnmordi  6789  nnmord  6790  nnaordex  6801  nnawordex  6802  nnm00  6803  eroveu  6900  ecopovtrn  6906  ecopovtrng  6909  th3qlem2  6912  th3q  6914  ecovcom  6916  ecovicom  6917  ecovass  6918  ecoviass  6919  ecovdi  6920  ecovidi  6921  exmidpw2en  7219  mapfi  7261  acneq  7558  addcanpig  7701  mulcanpig  7702  addcmpblnq  7734  addclnq  7742  mulclnq  7743  recexnq  7757  recmulnqg  7758  ltanqg  7767  ltmnqg  7768  ltexnqq  7775  enq0ref  7800  enq0tr  7801  addcmpblnq0  7810  mulnnnq0  7817  addclnq0  7818  mulclnq0  7819  distrnq0  7826  mulcomnq0  7827  addassnq0  7829  nq02m  7832  prarloclem3  7864  genipv  7876  genpassl  7891  genpassu  7892  addlocpr  7903  distrlem1prl  7949  distrlem1pru  7950  1idprl  7957  1idpru  7958  ltexprlemell  7965  ltexprlemelu  7966  ltexpri  7980  lteupri  7984  ltaprlem  7985  recexprlem1ssl  8000  recexprlem1ssu  8001  recexpr  8005  cauappcvgprlemm  8012  cauappcvgprlemdisj  8018  cauappcvgprlemloc  8019  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  cauappcvgprlem1  8026  cauappcvgprlemlim  8028  cauappcvgpr  8029  mulcmpblnrlemg  8107  addclsr  8120  mulclsr  8121  ltasrg  8137  negexsr  8139  recexgt0sr  8140  mulgt0sr  8145  mulextsr1  8148  srpospr  8150  caucvgsrlemgt1  8162  map2psrprg  8172  axaddrcl  8232  axmulrcl  8234  axaddcom  8237  axrnegex  8246  axprecex  8247  axcnre  8248  axpre-ltadd  8253  axpre-mulgt0  8254  axpre-mulext  8255  rereceu  8256  recriota  8257  axcaucvglemres  8266  readdcan  8466  cnegexlem1  8501  cnegex  8504  addcan  8506  negeq  8519  subadd  8529  addid0  8699  ine0  8721  rimul  8913  cru  8930  apreim  8931  recexap  8981  mulcanapd  8989  receuap  8999  divmulap  9005  rerecapb  9173  cju  9291  nnaddcl  9324  nnmulcl  9325  nnsub  9343  nnnn0addcl  9593  zaddcllempos  9681  zaddcl  9684  zdiv  9734  deceq1  9781  deceq2  9782  uzaddcl  9986  zq  10026  qreccl  10042  cnref1o  10051  xaddnemnf  10259  xaddnepnf  10260  xaddcom  10263  xnn0xadd0  10269  xnegdi  10270  xaddass  10271  xlt2add  10282  xlesubadd  10285  xleaddadd  10289  fzsuc2  10486  fzrevral  10512  fzshftral  10515  2ffzeq  10548  exfzdc  10659  exbtwnzlemshrink  10683  rebtwn2zlemshrink  10688  modqval  10761  modqmuladd  10803  modqmuladdnn0  10805  frecuzrdgrrn  10845  frec2uzrdg  10846  frecuzrdgrcl  10847  frecuzrdgsuc  10851  frecuzrdgrclt  10852  frecuzrdgg  10853  frecuzrdgsuctlem  10860  frecfzennn  10863  uzsinds  10881  iseqvalcbv  10896  seq3val  10897  seqvalcd  10898  seqovcd  10904  seq3caopr3  10928  seq3caopr2  10930  seqcaopr2g  10931  seq3f1olemp  10952  seqf1og  10958  seq3id  10962  seq3homo  10964  seq3z  10965  seqhomog  10967  seqfeq4g  10968  seq3distr  10969  expp1  10983  expnegap0  10984  expcllem  10987  expcl2lemap  10988  m1expcl2  10998  expap0  11006  mulexp  11015  expadd  11018  expmul  11021  leexp2r  11030  leexp1a  11031  bernneq  11098  expnbnd  11101  modqexp  11104  nn0ltexp2  11147  expcan  11154  apexp1  11156  facdiv  11176  faclbnd3  11181  faclbnd6  11182  bcval  11187  bcpasc  11204  bccl  11205  fz1eqb  11229  omgadd  11242  hashunlem  11244  hashfzo  11263  hashfzp1  11265  hashmap  11268  hashfibclem  11282  hashfibc  11283  hashf1  11287  iswrdinn0  11309  wrdnval  11335  eqwrd  11345  eqs1  11396  pfxeq  11468  ccatopth  11488  wrd2ind  11495  swrdccatin1  11497  swrdccatin2  11501  pfxccatin12lem2  11503  swrdccat3blem  11511  pfxccatid  11513  swrdccatin1d  11515  swrdccatin2d  11516  s2dmg  11562  shftfvalg  11583  shftfval  11586  cjth  11611  remim  11625  reim0b  11627  cjexp  11658  cnrecnv  11676  cvg1nlemcau  11750  cvg1nlemres  11751  recvguniq  11761  resqrexlemp1rp  11772  resqrexlemfp1  11775  resqrexlemlo  11779  resqrexlemgt0  11786  resqrexlemoverl  11787  resqrexlemglsq  11788  resqrexlemsqa  11790  resqrexlemex  11791  resqrex  11792  absexp  11845  recan  11875  climcn2  12075  subcn2  12077  summodc  12150  fsum3  12154  fsum3cvg3  12163  fsumrev  12210  fisum0diag2  12214  telfsumo  12233  fsumrelem  12238  binomlem  12250  binom  12251  binom1dif  12254  bcxmaslem1  12255  bcxmas  12256  isumshft  12257  divcnv  12264  arisum  12265  trireciplem  12267  expcnvap0  12269  expcnvre  12270  expcnv  12271  explecnv  12272  geosergap  12273  geolim  12278  geolim2  12279  geo2sum  12281  geo2lim  12283  geoisum  12284  geoisumr  12285  geoisum1  12286  geoisum1c  12287  cvgratnnlemsumlt  12295  cvgratz  12299  prodmodc  12345  fprodseq  12350  fprodcl2lem  12372  fprodfac  12382  fprodabs  12383  fprodrev  12386  eftvalcn  12424  efcvgfsum  12434  ege2le3  12438  efcj  12440  efaddlem  12441  efexp  12449  eftlub  12457  efgt1p2  12462  eflegeo  12468  sinval  12469  cosval  12470  demoivreALT  12541  divides  12556  dvdscmul  12585  dvds2ln  12591  dvdstr  12595  odd2np1lem  12639  odd2np1  12640  2tp1odd  12651  opeo  12664  omeo  12665  m1expe  12666  m1expo  12667  m1exp1  12668  divalglemnn  12685  divalglemeunn  12688  divalglemeuneg  12690  divalgmod  12694  ndvdssub  12697  bitsval  12710  bitsfzolem  12721  bitsinv1lem  12728  bitsinv1  12729  gcd0id  12756  bezoutlemnewy  12773  bezoutlema  12776  bezoutlemb  12777  bezoutlemex  12778  bezoutlemaz  12780  bezoutlembz  12781  gcdmultiple  12797  gcdmultiplez  12798  dvdsmulgcd  12802  rplpwr  12804  nn0seqcvgd  12819  dvdslcm  12847  lcmeq0  12849  lcmcl  12850  lcmneg  12852  lcmgcdlem  12855  lcmdvds  12857  lcmid  12858  lcmgcdeq  12861  coprmdvds  12870  mulgcddvds  12872  qredeq  12874  cncongr1  12881  cncongr2  12882  cncongrcoprm  12884  prmind2  12898  isprm6  12925  prmdvdsexp  12926  prmdvdsexpr  12928  sqrt2irr  12940  pw2dvdslemn  12943  pw2dvdseu  12946  oddpwdclemxy  12947  sqpweven  12953  2sqpwodd  12954  sqne2sq  12955  nn0gcdsq  12978  qden1elz  12983  phival  12991  dfphi2  12998  eulerthlemrprm  13007  eulerthlema  13008  prmdiv  13013  prmdiveq  13014  phisum  13019  odzval  13020  odzcllem  13021  odzdvds  13024  reumodprminv  13032  pythagtriplem3  13046  pythagtriplem18  13060  pythagtriplem19  13061  pclem0  13065  pclemub  13066  pclemdc  13067  pcprecl  13068  pcprendvds  13069  pcpremul  13072  pceulem  13073  pceu  13074  pczpre  13076  pcdiv  13081  pcqmul  13082  pcqcl  13085  pcexp  13088  pcxnn0cl  13089  pcxcl  13090  pcge0  13092  pcdvdsb  13099  pcneg  13104  pcabs  13105  pcgcd1  13107  pc2dvds  13109  pc11  13110  pcz  13111  pcprmpw2  13112  pcprmpw  13113  dvdsprmpweq  13114  dvdsprmpweqnn  13115  dvdsprmpweqle  13116  pcaddlem  13118  pcadd  13119  pcfac  13129  oddprmdvds  13133  prmpwdvds  13134  pockthi  13137  infpnlem2  13139  1arithlem1  13142  4sqlemffi  13175  4sqlem12  13181  2expltfac  13218  ballotfilemfval  13229  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemsv  13253  ballotfilemsf1o  13257  ballotfi  13282  ennnfonelemnn0  13313  ennnfonelemr  13314  f1ovscpbl  13633  imasaddvallemg  13636  ercpbl  13652  mgm1  13690  mgmidmo  13692  mgmlrid  13699  lidrideqd  13701  lidrididd  13702  grpinvalem  13705  grpinva  13706  gzsumfzval  13711  gzsumval2  13714  isnsgrp  13721  sgrpass  13723  sgrp1  13726  mndinvmod  13758  imasmnd2  13759  mnd1  13762  mnd1id  13763  mhmpropd  13773  mhmlin  13774  insubm  13792  mhmima  13798  gzsumwsubmcl  13801  gzsumwmhm  13803  grpinvex  13815  grppropd  13822  dfgrp2  13832  grpidd2  13846  grpinvval  13848  grpinvid1  13857  grplrinv  13862  grpidinv2  13863  grpidinv  13864  grplcan  13867  grpidssd  13881  grpinvssd  13882  dfgrp3mlem  13903  dfgrp3m  13904  grplactcnv  13907  grp1  13911  imasgrp2  13913  mhmlem  13917  mulgnn0gzsum  13931  mulginvcom  13950  mulgnn0ass  13961  mulgmodid  13964  issubg  13976  issubg2m  13992  issubg4m  13996  isnsg2  14006  nsgbi  14007  isnsg3  14010  elnmz  14011  nmzbi  14012  ghmlin  14051  ghmrn  14060  ghmnsgima  14071  conjghm  14079  conjnmz  14082  gzsumconst  14143  rngdi  14239  rngdir  14240  srglz  14289  srgisid  14290  srglmhm  14297  ringid  14331  ringinvnz1ne0  14354  ringinvnzdiv  14355  ring1  14364  ringlghm  14366  imasring  14369  dvdsrtr  14408  lringuplu  14503  issubrng  14507  issubrng2  14518  issubrg  14529  issubrg2  14549  rrgeq0i  14572  rrgeq0  14573  unitrrg  14576  domneq0  14581  lmodlema  14628  islmodd  14629  rmodislmodlem  14687  rmodislmod  14688  lssclg  14701  lss1d  14720  rnglidlmcl  14817  quscrng  14870  cnfldexp  14914  gsumfsum  14923  cnfldui  14924  expghmap  14942  zrhval  14952  zrhvalg  14953  znunit  14994  assalem  15003  txdis1cn  15379  cnmptcom  15399  psmettri2  15429  isxmet2d  15449  xmeteq0  15460  xmettri2  15462  elblps  15491  elbl  15492  blssps  15528  blss  15529  ssblex  15532  blin2  15533  metss2  15599  comet  15600  bdmopn  15605  txmetcnp  15619  blssioo  15654  divcnap  15666  mpomulcn  15667  expcn  15670  cncfval  15673  cncfi  15679  mulc1cncf  15690  cdivcncfap  15705  mulcncf  15709  expcncf  15710  cnopnap  15712  ellimc3apf  15761  cnlimci  15774  limccnpcntop  15776  limccnp2lem  15777  reldvg  15780  eldvap  15783  dvexp  15812  dvexp2  15813  dvrecap  15814  elplyr  15841  elplyd  15842  ply1termlem  15843  plymullem1  15849  plyadd  15852  plymul  15853  plycoeid3  15858  plycolemc  15859  plyco  15860  plycj  15862  dvply1  15866  dvply2g  15867  sin0pilem2  15883  logfac  15995  rpcxpmul2  16015  relogbcxpbap  16067  logbgcd1irr  16069  2irrexpq  16078  2irrexpqap  16080  log2tlbndlog2  16082  log2ublem2  16084  dvdsppwf1o  16103  mpodvdsmulf1o  16104  fsumdvdsmul  16105  sgmppw  16106  1sgmprm  16108  perfect  16115  lgsneg  16143  lgsdilem  16146  lgsdir  16154  lgsdilem2  16155  lgsdi  16156  lgsne0  16157  lgsdirnn0  16166  lgsdinn0  16167  gausslemma2dlem4  16183  lgseisenlem2  16190  lgseisenlem3  16191  lgseisenlem4  16192  lgsquadlem1  16196  lgsquadlem2  16197  lgsquad2lem2  16201  2lgs  16223  2sqlem6  16239  2sqlem8  16242  2sqlem9  16243  2sqlem10  16244  wlkeq  16595  wlkl1loop  16599  uspgr2wlkeq  16606  upgr2wlkdc  16618  clwwlknonmpo  16669  eupth2fi  16720  trilpolemclim  17085  trilpolemcl  17086  trilpolemisumle  17087  trilpolemeq1  17089  trilpolemlt1  17090  trilpo  17092  trirec0  17093  qdiff  17098  redcwlpo  17105  nconstwlpolemgt0  17114  nconstwlpo  17116  neapmkv  17118