Theorem oveq2 6068

Description: Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)

Assertion

Ref	Expression
oveq2	⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))

Proof of Theorem oveq2

Step	Hyp	Ref	Expression
1		opeq2 3890	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
2	1	fveq2d 5681	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘⟨𝐶, 𝐴⟩) = (𝐹‘⟨𝐶, 𝐵⟩))
3		df-ov 6063	. 2 ⊢ (𝐶𝐹𝐴) = (𝐹‘⟨𝐶, 𝐴⟩)
4		df-ov 6063	. 2 ⊢ (𝐶𝐹𝐵) = (𝐹‘⟨𝐶, 𝐵⟩)
5	2, 3, 4	3eqtr4g 2292	1 ⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))

Syntax hints:   → wi 4   = wceq 1398  ⟨cop 3698  ‘cfv 5359  (class class class)co 6060

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-v 2817  df-un 3218  df-sn 3701  df-pr 3702  df-op 3704  df-uni 3921  df-br 4116  df-iota 5319  df-fv 5367  df-ov 6063

This theorem is referenced by:  oveq12  6069  oveq2i  6071  oveq2d  6076  ovanraleqv  6084  ovrspc2v  6086  oveqrspc2v  6087  rspceov  6103  fovcld  6168  ovmpos  6187  ov2gf  6188  ovi3  6201  caovclg  6217  caovcomg  6220  caovassg  6223  caovcang  6226  caovcan  6229  caovordig  6230  caovordg  6232  caovord  6236  caovdig  6239  caovdirg  6242  caovimo  6258  suppssov1  6274  off  6290  caofid0l  6304  caofid2  6307  caofdig  6311  suppofss1dcl  6479  suppofss2dcl  6480  omv  6703  oeiv  6704  oasuc  6712  oawordriexmid  6718  omsuc  6720  nna0r  6726  nnm0r  6727  nnacl  6728  nnmcl  6729  nnacom  6732  nnaass  6733  nndi  6734  nnmass  6735  nnmsucr  6736  nnmcom  6737  nnaordi  6756  nnaord  6757  nnmordi  6764  nnmord  6765  nnaordex  6776  nnawordex  6777  nnm00  6778  eroveu  6875  ecopovtrn  6881  ecopovtrng  6884  th3qlem2  6887  th3q  6889  ecovcom  6891  ecovicom  6892  ecovass  6893  ecoviass  6894  ecovdi  6895  ecovidi  6896  exmidpw2en  7187  mapfi  7229  acneq  7524  addcanpig  7667  mulcanpig  7668  addcmpblnq  7700  addclnq  7708  mulclnq  7709  recexnq  7723  recmulnqg  7724  ltanqg  7733  ltmnqg  7734  ltexnqq  7741  enq0ref  7766  enq0tr  7767  addcmpblnq0  7776  mulnnnq0  7783  addclnq0  7784  mulclnq0  7785  distrnq0  7792  mulcomnq0  7793  addassnq0  7795  nq02m  7798  prarloclem3  7830  genipv  7842  genpassl  7857  genpassu  7858  addlocpr  7869  distrlem1prl  7915  distrlem1pru  7916  1idprl  7923  1idpru  7924  ltexprlemell  7931  ltexprlemelu  7932  ltexpri  7946  lteupri  7950  ltaprlem  7951  recexprlem1ssl  7966  recexprlem1ssu  7967  recexpr  7971  cauappcvgprlemm  7978  cauappcvgprlemdisj  7984  cauappcvgprlemloc  7985  cauappcvgprlemladdru  7989  cauappcvgprlemladdrl  7990  cauappcvgprlem1  7992  cauappcvgprlemlim  7994  cauappcvgpr  7995  mulcmpblnrlemg  8073  addclsr  8086  mulclsr  8087  ltasrg  8103  negexsr  8105  recexgt0sr  8106  mulgt0sr  8111  mulextsr1  8114  srpospr  8116  caucvgsrlemgt1  8128  map2psrprg  8138  axaddrcl  8198  axmulrcl  8200  axaddcom  8203  axrnegex  8212  axprecex  8213  axcnre  8214  axpre-ltadd  8219  axpre-mulgt0  8220  axpre-mulext  8221  rereceu  8222  recriota  8223  axcaucvglemres  8232  readdcan  8432  cnegexlem1  8467  cnegex  8470  addcan  8472  negeq  8485  subadd  8495  addid0  8665  ine0  8687  rimul  8879  cru  8896  apreim  8897  recexap  8947  mulcanapd  8955  receuap  8965  divmulap  8971  rerecapb  9139  cju  9257  nnaddcl  9279  nnmulcl  9280  nnsub  9298  nnnn0addcl  9548  zaddcllempos  9636  zaddcl  9639  zdiv  9689  deceq1  9736  deceq2  9737  uzaddcl  9941  zq  9981  qreccl  9997  cnref1o  10006  xaddnemnf  10214  xaddnepnf  10215  xaddcom  10218  xnn0xadd0  10224  xnegdi  10225  xaddass  10226  xlt2add  10237  xlesubadd  10240  xleaddadd  10244  fzsuc2  10440  fzrevral  10466  fzshftral  10469  2ffzeq  10502  exfzdc  10613  exbtwnzlemshrink  10637  rebtwn2zlemshrink  10642  modqval  10715  modqmuladd  10757  modqmuladdnn0  10759  frecuzrdgrrn  10799  frec2uzrdg  10800  frecuzrdgrcl  10801  frecuzrdgsuc  10805  frecuzrdgrclt  10806  frecuzrdgg  10807  frecuzrdgsuctlem  10814  frecfzennn  10817  uzsinds  10835  iseqvalcbv  10850  seq3val  10851  seqvalcd  10852  seqovcd  10858  seq3caopr3  10882  seq3caopr2  10884  seqcaopr2g  10885  seq3f1olemp  10906  seqf1og  10912  seq3id  10916  seq3homo  10918  seq3z  10919  seqhomog  10921  seqfeq4g  10922  seq3distr  10923  expp1  10937  expnegap0  10938  expcllem  10941  expcl2lemap  10942  m1expcl2  10952  expap0  10960  mulexp  10969  expadd  10972  expmul  10975  leexp2r  10984  leexp1a  10985  bernneq  11052  expnbnd  11055  modqexp  11058  nn0ltexp2  11101  expcan  11108  apexp1  11110  facdiv  11130  faclbnd3  11135  faclbnd6  11136  bcval  11141  bcpasc  11158  bccl  11159  fz1eqb  11183  omgadd  11196  hashunlem  11198  hashfzo  11217  hashfzp1  11219  hashmap  11222  hashfibclem  11236  hashfibc  11237  iswrdinn0  11259  wrdnval  11285  eqwrd  11295  eqs1  11346  pfxeq  11418  ccatopth  11438  wrd2ind  11445  swrdccatin1  11447  swrdccatin2  11451  pfxccatin12lem2  11453  swrdccat3blem  11461  pfxccatid  11463  swrdccatin1d  11465  swrdccatin2d  11466  s2dmg  11512  shftfvalg  11533  shftfval  11536  cjth  11561  remim  11575  reim0b  11577  cjexp  11608  cnrecnv  11626  cvg1nlemcau  11700  cvg1nlemres  11701  recvguniq  11711  resqrexlemp1rp  11722  resqrexlemfp1  11725  resqrexlemlo  11729  resqrexlemgt0  11736  resqrexlemoverl  11737  resqrexlemglsq  11738  resqrexlemsqa  11740  resqrexlemex  11741  resqrex  11742  absexp  11795  recan  11825  climcn2  12025  subcn2  12027  summodc  12100  fsum3  12104  fsum3cvg3  12113  fsumrev  12160  fisum0diag2  12164  telfsumo  12183  fsumrelem  12188  binomlem  12200  binom  12201  binom1dif  12204  bcxmaslem1  12205  bcxmas  12206  isumshft  12207  divcnv  12214  arisum  12215  trireciplem  12217  expcnvap0  12219  expcnvre  12220  expcnv  12221  explecnv  12222  geosergap  12223  geolim  12228  geolim2  12229  geo2sum  12231  geo2lim  12233  geoisum  12234  geoisumr  12235  geoisum1  12236  geoisum1c  12237  cvgratnnlemsumlt  12245  cvgratz  12249  prodmodc  12295  fprodseq  12300  fprodcl2lem  12322  fprodfac  12332  fprodabs  12333  fprodrev  12336  eftvalcn  12374  efcvgfsum  12384  ege2le3  12388  efcj  12390  efaddlem  12391  efexp  12399  eftlub  12407  efgt1p2  12412  eflegeo  12418  sinval  12419  cosval  12420  demoivreALT  12491  divides  12506  dvdscmul  12535  dvds2ln  12541  dvdstr  12545  odd2np1lem  12589  odd2np1  12590  2tp1odd  12601  opeo  12614  omeo  12615  m1expe  12616  m1expo  12617  m1exp1  12618  divalglemnn  12635  divalglemeunn  12638  divalglemeuneg  12640  divalgmod  12644  ndvdssub  12647  bitsval  12660  bitsfzolem  12671  bitsinv1lem  12678  bitsinv1  12679  gcd0id  12706  bezoutlemnewy  12723  bezoutlema  12726  bezoutlemb  12727  bezoutlemex  12728  bezoutlemaz  12730  bezoutlembz  12731  gcdmultiple  12747  gcdmultiplez  12748  dvdsmulgcd  12752  rplpwr  12754  nn0seqcvgd  12769  dvdslcm  12797  lcmeq0  12799  lcmcl  12800  lcmneg  12802  lcmgcdlem  12805  lcmdvds  12807  lcmid  12808  lcmgcdeq  12811  coprmdvds  12820  mulgcddvds  12822  qredeq  12824  cncongr1  12831  cncongr2  12832  cncongrcoprm  12834  prmind2  12848  isprm6  12875  prmdvdsexp  12876  prmdvdsexpr  12878  sqrt2irr  12890  pw2dvdslemn  12893  pw2dvdseu  12896  oddpwdclemxy  12897  sqpweven  12903  2sqpwodd  12904  sqne2sq  12905  nn0gcdsq  12928  qden1elz  12933  phival  12941  dfphi2  12948  eulerthlemrprm  12957  eulerthlema  12958  prmdiv  12963  prmdiveq  12964  phisum  12969  odzval  12970  odzcllem  12971  odzdvds  12974  reumodprminv  12982  pythagtriplem3  12996  pythagtriplem18  13010  pythagtriplem19  13011  pclem0  13015  pclemub  13016  pclemdc  13017  pcprecl  13018  pcprendvds  13019  pcpremul  13022  pceulem  13023  pceu  13024  pczpre  13026  pcdiv  13031  pcqmul  13032  pcqcl  13035  pcexp  13038  pcxnn0cl  13039  pcxcl  13040  pcge0  13042  pcdvdsb  13049  pcneg  13054  pcabs  13055  pcgcd1  13057  pc2dvds  13059  pc11  13060  pcz  13061  pcprmpw2  13062  pcprmpw  13063  dvdsprmpweq  13064  dvdsprmpweqnn  13065  dvdsprmpweqle  13066  pcaddlem  13068  pcadd  13069  pcfac  13079  oddprmdvds  13083  prmpwdvds  13084  pockthi  13087  infpnlem2  13089  1arithlem1  13092  4sqlemffi  13125  4sqlem12  13131  2expltfac  13168  ballotfilemfval  13179  ballotfilemfc0  13182  ballotfilemfcc  13183  ballotfilemsv  13203  ballotfilemsf1o  13207  ballotfi  13232  ennnfonelemnn0  13263  ennnfonelemr  13264  f1ovscpbl  13582  imasaddvallemg  13585  ercpbl  13601  mgm1  13639  mgmidmo  13641  mgmlrid  13648  lidrideqd  13650  lidrididd  13651  grpinvalem  13654  grpinva  13655  gsumfzval  13660  gsumval2  13666  isnsgrp  13675  sgrpass  13677  sgrp1  13680  mndinvmod  13712  imasmnd2  13713  mnd1  13716  mnd1id  13717  mhmpropd  13727  mhmlin  13728  insubm  13746  mhmima  13752  gsumwsubmcl  13757  gsumwmhm  13759  grpinvex  13771  grppropd  13778  dfgrp2  13788  grpidd2  13802  grpinvval  13804  grpinvid1  13813  grplrinv  13818  grpidinv2  13819  grpidinv  13820  grplcan  13823  grpidssd  13837  grpinvssd  13838  dfgrp3mlem  13859  dfgrp3m  13860  grplactcnv  13863  grp1  13867  imasgrp2  13869  mhmlem  13873  mulgnn0gsum  13887  mulginvcom  13906  mulgnn0ass  13917  mulgmodid  13920  issubg  13932  issubg2m  13948  issubg4m  13952  isnsg2  13962  nsgbi  13963  isnsg3  13966  elnmz  13967  nmzbi  13968  ghmlin  14007  ghmrn  14016  ghmnsgima  14027  conjghm  14035  conjnmz  14038  gsumfzconst  14100  rngdi  14185  rngdir  14186  srglz  14234  srgisid  14235  srglmhm  14242  ringid  14275  ringinvnz1ne0  14298  ringinvnzdiv  14299  ring1  14308  ringlghm  14310  imasring  14313  dvdsrtr  14352  lringuplu  14447  issubrng  14451  issubrng2  14462  issubrg  14473  issubrg2  14493  rrgeq0i  14516  rrgeq0  14517  unitrrg  14520  domneq0  14525  lmodlema  14572  islmodd  14573  rmodislmodlem  14630  rmodislmod  14631  lssclg  14644  lss1d  14663  rnglidlmcl  14760  quscrng  14813  cnfldexp  14857  gsumfzfsumlemm  14867  cnfldui  14869  expghmap  14887  zrhval  14897  zrhvalg  14898  znunit  14939  txdis1cn  15275  cnmptcom  15295  psmettri2  15325  isxmet2d  15345  xmeteq0  15356  xmettri2  15358  elblps  15387  elbl  15388  blssps  15424  blss  15425  ssblex  15428  blin2  15429  metss2  15495  comet  15496  bdmopn  15501  txmetcnp  15515  blssioo  15550  divcnap  15562  mpomulcn  15563  expcn  15566  cncfval  15569  cncfi  15575  mulc1cncf  15586  cdivcncfap  15601  mulcncf  15605  expcncf  15606  cnopnap  15608  ellimc3apf  15657  cnlimci  15670  limccnpcntop  15672  limccnp2lem  15673  reldvg  15676  eldvap  15679  dvexp  15708  dvexp2  15709  dvrecap  15710  elplyr  15737  elplyd  15738  ply1termlem  15739  plymullem1  15745  plyadd  15748  plymul  15749  plycoeid3  15754  plycolemc  15755  plyco  15756  plycj  15758  dvply1  15762  dvply2g  15763  sin0pilem2  15779  rpcxpmul2  15910  relogbcxpbap  15962  logbgcd1irr  15964  2irrexpq  15973  2irrexpqap  15975  dvdsppwf1o  15989  mpodvdsmulf1o  15990  fsumdvdsmul  15991  sgmppw  15992  1sgmprm  15994  perfect  16001  lgsneg  16029  lgsdilem  16032  lgsdir  16040  lgsdilem2  16041  lgsdi  16042  lgsne0  16043  lgsdirnn0  16052  lgsdinn0  16053  gausslemma2dlem4  16069  lgseisenlem2  16076  lgseisenlem3  16077  lgseisenlem4  16078  lgsquadlem1  16082  lgsquadlem2  16083  lgsquad2lem2  16087  2lgs  16109  2sqlem6  16125  2sqlem8  16128  2sqlem9  16129  2sqlem10  16130  wlkeq  16481  wlkl1loop  16485  uspgr2wlkeq  16492  upgr2wlkdc  16504  clwwlknonmpo  16555  eupth2fi  16606  trilpolemclim  16962  trilpolemcl  16963  trilpolemisumle  16964  trilpolemeq1  16966  trilpolemlt1  16967  trilpo  16969  trirec0  16970  qdiff  16975  redcwlpo  16982  nconstwlpolemgt0  16991  nconstwlpo  16993  neapmkv  16995