Theorem oveq2 5861

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 3766	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
2	1	fveq2d 5500	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘⟨𝐶, 𝐴⟩) = (𝐹‘⟨𝐶, 𝐵⟩))
3		df-ov 5856	. 2 ⊢ (𝐶𝐹𝐴) = (𝐹‘⟨𝐶, 𝐴⟩)
4		df-ov 5856	. 2 ⊢ (𝐶𝐹𝐵) = (𝐹‘⟨𝐶, 𝐵⟩)
5	2, 3, 4	3eqtr4g 2228	1 ⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))

Syntax hints:   → wi 4   = wceq 1348  ⟨cop 3586  ‘cfv 5198  (class class class)co 5853

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-rex 2454  df-v 2732  df-un 3125  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-br 3990  df-iota 5160  df-fv 5206  df-ov 5856

This theorem is referenced by:  oveq12  5862  oveq2i  5864  oveq2d  5869  ovanraleqv  5877  ovrspc2v  5879  oveqrspc2v  5880  rspceov  5895  fovcl  5958  ovmpos  5976  ov2gf  5977  ovi3  5989  caovclg  6005  caovcomg  6008  caovassg  6011  caovcang  6014  caovcan  6017  caovordig  6018  caovordg  6020  caovord  6024  caovdig  6027  caovdirg  6030  caovimo  6046  suppssov1  6058  off  6073  omv  6434  oeiv  6435  oasuc  6443  oawordriexmid  6449  omsuc  6451  nna0r  6457  nnm0r  6458  nnacl  6459  nnmcl  6460  nnacom  6463  nnaass  6464  nndi  6465  nnmass  6466  nnmsucr  6467  nnmcom  6468  nnaordi  6487  nnaord  6488  nnmordi  6495  nnmord  6496  nnaordex  6507  nnawordex  6508  nnm00  6509  eroveu  6604  ecopovtrn  6610  ecopovtrng  6613  th3qlem2  6616  th3q  6618  ecovcom  6620  ecovicom  6621  ecovass  6622  ecoviass  6623  ecovdi  6624  ecovidi  6625  addcanpig  7296  mulcanpig  7297  addcmpblnq  7329  addclnq  7337  mulclnq  7338  recexnq  7352  recmulnqg  7353  ltanqg  7362  ltmnqg  7363  ltexnqq  7370  enq0ref  7395  enq0tr  7396  addcmpblnq0  7405  mulnnnq0  7412  addclnq0  7413  mulclnq0  7414  distrnq0  7421  mulcomnq0  7422  addassnq0  7424  nq02m  7427  prarloclem3  7459  genipv  7471  genpassl  7486  genpassu  7487  addlocpr  7498  distrlem1prl  7544  distrlem1pru  7545  1idprl  7552  1idpru  7553  ltexprlemell  7560  ltexprlemelu  7561  ltexpri  7575  lteupri  7579  ltaprlem  7580  recexprlem1ssl  7595  recexprlem1ssu  7596  recexpr  7600  cauappcvgprlemm  7607  cauappcvgprlemdisj  7613  cauappcvgprlemloc  7614  cauappcvgprlemladdru  7618  cauappcvgprlemladdrl  7619  cauappcvgprlem1  7621  cauappcvgprlemlim  7623  cauappcvgpr  7624  mulcmpblnrlemg  7702  addclsr  7715  mulclsr  7716  ltasrg  7732  negexsr  7734  recexgt0sr  7735  mulgt0sr  7740  mulextsr1  7743  srpospr  7745  caucvgsrlemgt1  7757  map2psrprg  7767  axaddrcl  7827  axmulrcl  7829  axaddcom  7832  axrnegex  7841  axprecex  7842  axcnre  7843  axpre-ltadd  7848  axpre-mulgt0  7849  axpre-mulext  7850  rereceu  7851  recriota  7852  axcaucvglemres  7861  readdcan  8059  cnegexlem1  8094  cnegex  8097  addcan  8099  negeq  8112  subadd  8122  addid0  8292  ine0  8313  rimul  8504  cru  8521  apreim  8522  recexap  8571  mulcanapd  8579  receuap  8587  divmulap  8592  cju  8877  nnaddcl  8898  nnmulcl  8899  nnsub  8917  nnnn0addcl  9165  zaddcllempos  9249  zaddcl  9252  zdiv  9300  deceq1  9347  deceq2  9348  uzaddcl  9545  zq  9585  qreccl  9601  cnref1o  9609  xaddnemnf  9814  xaddnepnf  9815  xaddcom  9818  xnn0xadd0  9824  xnegdi  9825  xaddass  9826  xlt2add  9837  xlesubadd  9840  xleaddadd  9844  fzsuc2  10035  fzrevral  10061  fzshftral  10064  2ffzeq  10097  exfzdc  10196  exbtwnzlemshrink  10205  rebtwn2zlemshrink  10210  modqval  10280  modqmuladd  10322  modqmuladdnn0  10324  frecuzrdgrrn  10364  frec2uzrdg  10365  frecuzrdgrcl  10366  frecuzrdgsuc  10370  frecuzrdgrclt  10371  frecuzrdgg  10372  frecuzrdgsuctlem  10379  frecfzennn  10382  uzsinds  10398  iseqvalcbv  10413  seq3val  10414  seqvalcd  10415  seqovcd  10419  seq3caopr3  10437  seq3caopr2  10438  seq3f1olemp  10458  seq3id  10464  seq3homo  10466  seq3z  10467  seq3distr  10469  expp1  10483  expnegap0  10484  expcllem  10487  expcl2lemap  10488  m1expcl2  10498  expap0  10506  mulexp  10515  expadd  10518  expmul  10521  leexp2r  10530  leexp1a  10531  bernneq  10596  expnbnd  10599  modqexp  10602  nn0ltexp2  10644  expcan  10650  apexp1  10652  facdiv  10672  faclbnd3  10677  faclbnd6  10678  bcval  10683  bcpasc  10700  bccl  10701  fz1eqb  10725  omgadd  10737  hashunlem  10739  hashfzo  10757  hashfzp1  10759  shftfvalg  10782  shftfval  10785  cjth  10810  remim  10824  reim0b  10826  cjexp  10857  cnrecnv  10874  cvg1nlemcau  10948  cvg1nlemres  10949  recvguniq  10959  resqrexlemp1rp  10970  resqrexlemfp1  10973  resqrexlemlo  10977  resqrexlemgt0  10984  resqrexlemoverl  10985  resqrexlemglsq  10986  resqrexlemsqa  10988  resqrexlemex  10989  resqrex  10990  absexp  11043  recan  11073  climcn2  11272  subcn2  11274  summodc  11346  fsum3  11350  fsum3cvg3  11359  fsumrev  11406  fisum0diag2  11410  telfsumo  11429  fsumrelem  11434  binomlem  11446  binom  11447  binom1dif  11450  bcxmaslem1  11451  bcxmas  11452  isumshft  11453  divcnv  11460  arisum  11461  trireciplem  11463  expcnvap0  11465  expcnvre  11466  expcnv  11467  explecnv  11468  geosergap  11469  geolim  11474  geolim2  11475  geo2sum  11477  geo2lim  11479  geoisum  11480  geoisumr  11481  geoisum1  11482  geoisum1c  11483  cvgratnnlemsumlt  11491  cvgratz  11495  prodmodc  11541  fprodseq  11546  fprodcl2lem  11568  fprodfac  11578  fprodabs  11579  fprodrev  11582  eftvalcn  11620  efcvgfsum  11630  ege2le3  11634  efcj  11636  efaddlem  11637  efexp  11645  eftlub  11653  efgt1p2  11658  eflegeo  11664  sinval  11665  cosval  11666  demoivreALT  11736  divides  11751  dvdscmul  11780  dvds2ln  11786  dvdstr  11790  odd2np1lem  11831  odd2np1  11832  2tp1odd  11843  opeo  11856  omeo  11857  m1expe  11858  m1expo  11859  m1exp1  11860  divalglemnn  11877  divalglemeunn  11880  divalglemeuneg  11882  divalgmod  11886  ndvdssub  11889  gcd0id  11934  bezoutlemnewy  11951  bezoutlema  11954  bezoutlemb  11955  bezoutlemex  11956  bezoutlemaz  11958  bezoutlembz  11959  gcdmultiple  11975  gcdmultiplez  11976  dvdsmulgcd  11980  rplpwr  11982  nn0seqcvgd  11995  dvdslcm  12023  lcmeq0  12025  lcmcl  12026  lcmneg  12028  lcmgcdlem  12031  lcmdvds  12033  lcmid  12034  lcmgcdeq  12037  coprmdvds  12046  mulgcddvds  12048  qredeq  12050  cncongr1  12057  cncongr2  12058  cncongrcoprm  12060  prmind2  12074  isprm6  12101  prmdvdsexp  12102  prmdvdsexpr  12104  sqrt2irr  12116  pw2dvdslemn  12119  pw2dvdseu  12122  oddpwdclemxy  12123  sqpweven  12129  2sqpwodd  12130  sqne2sq  12131  nn0gcdsq  12154  qden1elz  12159  phival  12167  dfphi2  12174  eulerthlemrprm  12183  eulerthlema  12184  prmdiv  12189  prmdiveq  12190  phisum  12194  odzval  12195  odzcllem  12196  odzdvds  12199  reumodprminv  12207  pythagtriplem3  12221  pythagtriplem18  12235  pythagtriplem19  12236  pclem0  12240  pclemub  12241  pclemdc  12242  pcprecl  12243  pcprendvds  12244  pcpremul  12247  pceulem  12248  pceu  12249  pczpre  12251  pcdiv  12256  pcqmul  12257  pcqcl  12260  pcexp  12263  pcxnn0cl  12264  pcxcl  12265  pcge0  12266  pcdvdsb  12273  pcneg  12278  pcabs  12279  pcgcd1  12281  pc2dvds  12283  pc11  12284  pcz  12285  pcprmpw2  12286  pcprmpw  12287  dvdsprmpweq  12288  dvdsprmpweqnn  12289  dvdsprmpweqle  12290  pcaddlem  12292  pcadd  12293  pcfac  12302  oddprmdvds  12306  prmpwdvds  12307  pockthi  12310  infpnlem2  12312  1arithlem1  12315  ennnfonelemnn0  12377  ennnfonelemr  12378  mgm1  12624  mgmidmo  12626  mgmlrid  12633  lidrideqd  12635  lidrididd  12636  grprinvlem  12639  grprinvd  12640  isnsgrp  12647  sgrpass  12649  sgrp1  12651  mndinvmod  12678  mnd1  12679  mnd1id  12680  mhmpropd  12689  mhmlin  12690  insubm  12703  mhmima  12706  grpinvex  12718  grppropd  12724  dfgrp2  12732  grpidd2  12744  grpinvval  12746  grpinvid1  12754  grplrinv  12757  grpidinv2  12758  grpidinv  12759  grplcan  12761  txdis1cn  13072  cnmptcom  13092  psmettri2  13122  isxmet2d  13142  xmeteq0  13153  xmettri2  13155  elblps  13184  elbl  13185  blssps  13221  blss  13222  ssblex  13225  blin2  13226  metss2  13292  comet  13293  bdmopn  13298  txmetcnp  13312  blssioo  13339  divcnap  13349  cncfval  13353  cncfi  13359  mulc1cncf  13370  cdivcncfap  13381  mulcncf  13385  expcncf  13386  cnopnap  13388  ellimc3apf  13423  cnlimci  13436  limccnpcntop  13438  limccnp2lem  13439  reldvg  13442  eldvap  13445  dvexp  13469  dvexp2  13470  dvrecap  13471  sin0pilem2  13497  relogbcxpbap  13677  logbgcd1irr  13679  2irrexpq  13688  2irrexpqap  13690  lgsneg  13719  lgsdilem  13722  lgsdir  13730  lgsdilem2  13731  lgsdi  13732  lgsne0  13733  lgsdirnn0  13742  lgsdinn0  13743  2sqlem6  13750  2sqlem8  13753  2sqlem9  13754  2sqlem10  13755  trilpolemclim  14068  trilpolemcl  14069  trilpolemisumle  14070  trilpolemeq1  14072  trilpolemlt1  14073  trilpo  14075  trirec0  14076  redcwlpo  14087  nconstwlpolemgt0  14095  nconstwlpo  14097  neapmkv  14099