Theorem oveq2 5850

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 3759	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
2	1	fveq2d 5490	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘⟨𝐶, 𝐴⟩) = (𝐹‘⟨𝐶, 𝐵⟩))
3		df-ov 5845	. 2 ⊢ (𝐶𝐹𝐴) = (𝐹‘⟨𝐶, 𝐴⟩)
4		df-ov 5845	. 2 ⊢ (𝐶𝐹𝐵) = (𝐹‘⟨𝐶, 𝐵⟩)
5	2, 3, 4	3eqtr4g 2224	1 ⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))

Syntax hints:   → wi 4   = wceq 1343  ⟨cop 3579  ‘cfv 5188  (class class class)co 5842

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 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-rex 2450  df-v 2728  df-un 3120  df-sn 3582  df-pr 3583  df-op 3585  df-uni 3790  df-br 3983  df-iota 5153  df-fv 5196  df-ov 5845

This theorem is referenced by:  oveq12  5851  oveq2i  5853  oveq2d  5858  ovanraleqv  5866  ovrspc2v  5868  oveqrspc2v  5869  rspceov  5884  fovcl  5947  ovmpos  5965  ov2gf  5966  ovi3  5978  caovclg  5994  caovcomg  5997  caovassg  6000  caovcang  6003  caovcan  6006  caovordig  6007  caovordg  6009  caovord  6013  caovdig  6016  caovdirg  6019  caovimo  6035  suppssov1  6047  off  6062  omv  6423  oeiv  6424  oasuc  6432  oawordriexmid  6438  omsuc  6440  nna0r  6446  nnm0r  6447  nnacl  6448  nnmcl  6449  nnacom  6452  nnaass  6453  nndi  6454  nnmass  6455  nnmsucr  6456  nnmcom  6457  nnaordi  6476  nnaord  6477  nnmordi  6484  nnmord  6485  nnaordex  6495  nnawordex  6496  nnm00  6497  eroveu  6592  ecopovtrn  6598  ecopovtrng  6601  th3qlem2  6604  th3q  6606  ecovcom  6608  ecovicom  6609  ecovass  6610  ecoviass  6611  ecovdi  6612  ecovidi  6613  addcanpig  7275  mulcanpig  7276  addcmpblnq  7308  addclnq  7316  mulclnq  7317  recexnq  7331  recmulnqg  7332  ltanqg  7341  ltmnqg  7342  ltexnqq  7349  enq0ref  7374  enq0tr  7375  addcmpblnq0  7384  mulnnnq0  7391  addclnq0  7392  mulclnq0  7393  distrnq0  7400  mulcomnq0  7401  addassnq0  7403  nq02m  7406  prarloclem3  7438  genipv  7450  genpassl  7465  genpassu  7466  addlocpr  7477  distrlem1prl  7523  distrlem1pru  7524  1idprl  7531  1idpru  7532  ltexprlemell  7539  ltexprlemelu  7540  ltexpri  7554  lteupri  7558  ltaprlem  7559  recexprlem1ssl  7574  recexprlem1ssu  7575  recexpr  7579  cauappcvgprlemm  7586  cauappcvgprlemdisj  7592  cauappcvgprlemloc  7593  cauappcvgprlemladdru  7597  cauappcvgprlemladdrl  7598  cauappcvgprlem1  7600  cauappcvgprlemlim  7602  cauappcvgpr  7603  mulcmpblnrlemg  7681  addclsr  7694  mulclsr  7695  ltasrg  7711  negexsr  7713  recexgt0sr  7714  mulgt0sr  7719  mulextsr1  7722  srpospr  7724  caucvgsrlemgt1  7736  map2psrprg  7746  axaddrcl  7806  axmulrcl  7808  axaddcom  7811  axrnegex  7820  axprecex  7821  axcnre  7822  axpre-ltadd  7827  axpre-mulgt0  7828  axpre-mulext  7829  rereceu  7830  recriota  7831  axcaucvglemres  7840  readdcan  8038  cnegexlem1  8073  cnegex  8076  addcan  8078  negeq  8091  subadd  8101  addid0  8271  ine0  8292  rimul  8483  cru  8500  apreim  8501  recexap  8550  mulcanapd  8558  receuap  8566  divmulap  8571  cju  8856  nnaddcl  8877  nnmulcl  8878  nnsub  8896  nnnn0addcl  9144  zaddcllempos  9228  zaddcl  9231  zdiv  9279  deceq1  9326  deceq2  9327  uzaddcl  9524  zq  9564  qreccl  9580  cnref1o  9588  xaddnemnf  9793  xaddnepnf  9794  xaddcom  9797  xnn0xadd0  9803  xnegdi  9804  xaddass  9805  xlt2add  9816  xlesubadd  9819  xleaddadd  9823  fzsuc2  10014  fzrevral  10040  fzshftral  10043  2ffzeq  10076  exfzdc  10175  exbtwnzlemshrink  10184  rebtwn2zlemshrink  10189  modqval  10259  modqmuladd  10301  modqmuladdnn0  10303  frecuzrdgrrn  10343  frec2uzrdg  10344  frecuzrdgrcl  10345  frecuzrdgsuc  10349  frecuzrdgrclt  10350  frecuzrdgg  10351  frecuzrdgsuctlem  10358  frecfzennn  10361  uzsinds  10377  iseqvalcbv  10392  seq3val  10393  seqvalcd  10394  seqovcd  10398  seq3caopr3  10416  seq3caopr2  10417  seq3f1olemp  10437  seq3id  10443  seq3homo  10445  seq3z  10446  seq3distr  10448  expp1  10462  expnegap0  10463  expcllem  10466  expcl2lemap  10467  m1expcl2  10477  expap0  10485  mulexp  10494  expadd  10497  expmul  10500  leexp2r  10509  leexp1a  10510  bernneq  10575  expnbnd  10578  modqexp  10581  nn0ltexp2  10623  expcan  10629  apexp1  10631  facdiv  10651  faclbnd3  10656  faclbnd6  10657  bcval  10662  bcpasc  10679  bccl  10680  fz1eqb  10704  omgadd  10715  hashunlem  10717  hashfzo  10735  hashfzp1  10737  shftfvalg  10760  shftfval  10763  cjth  10788  remim  10802  reim0b  10804  cjexp  10835  cnrecnv  10852  cvg1nlemcau  10926  cvg1nlemres  10927  recvguniq  10937  resqrexlemp1rp  10948  resqrexlemfp1  10951  resqrexlemlo  10955  resqrexlemgt0  10962  resqrexlemoverl  10963  resqrexlemglsq  10964  resqrexlemsqa  10966  resqrexlemex  10967  resqrex  10968  absexp  11021  recan  11051  climcn2  11250  subcn2  11252  summodc  11324  fsum3  11328  fsum3cvg3  11337  fsumrev  11384  fisum0diag2  11388  telfsumo  11407  fsumrelem  11412  binomlem  11424  binom  11425  binom1dif  11428  bcxmaslem1  11429  bcxmas  11430  isumshft  11431  divcnv  11438  arisum  11439  trireciplem  11441  expcnvap0  11443  expcnvre  11444  expcnv  11445  explecnv  11446  geosergap  11447  geolim  11452  geolim2  11453  geo2sum  11455  geo2lim  11457  geoisum  11458  geoisumr  11459  geoisum1  11460  geoisum1c  11461  cvgratnnlemsumlt  11469  cvgratz  11473  prodmodc  11519  fprodseq  11524  fprodcl2lem  11546  fprodfac  11556  fprodabs  11557  fprodrev  11560  eftvalcn  11598  efcvgfsum  11608  ege2le3  11612  efcj  11614  efaddlem  11615  efexp  11623  eftlub  11631  efgt1p2  11636  eflegeo  11642  sinval  11643  cosval  11644  demoivreALT  11714  divides  11729  dvdscmul  11758  dvds2ln  11764  dvdstr  11768  odd2np1lem  11809  odd2np1  11810  2tp1odd  11821  opeo  11834  omeo  11835  m1expe  11836  m1expo  11837  m1exp1  11838  divalglemnn  11855  divalglemeunn  11858  divalglemeuneg  11860  divalgmod  11864  ndvdssub  11867  gcd0id  11912  bezoutlemnewy  11929  bezoutlema  11932  bezoutlemb  11933  bezoutlemex  11934  bezoutlemaz  11936  bezoutlembz  11937  gcdmultiple  11953  gcdmultiplez  11954  dvdsmulgcd  11958  rplpwr  11960  nn0seqcvgd  11973  dvdslcm  12001  lcmeq0  12003  lcmcl  12004  lcmneg  12006  lcmgcdlem  12009  lcmdvds  12011  lcmid  12012  lcmgcdeq  12015  coprmdvds  12024  mulgcddvds  12026  qredeq  12028  cncongr1  12035  cncongr2  12036  cncongrcoprm  12038  prmind2  12052  isprm6  12079  prmdvdsexp  12080  prmdvdsexpr  12082  sqrt2irr  12094  pw2dvdslemn  12097  pw2dvdseu  12100  oddpwdclemxy  12101  sqpweven  12107  2sqpwodd  12108  sqne2sq  12109  nn0gcdsq  12132  qden1elz  12137  phival  12145  dfphi2  12152  eulerthlemrprm  12161  eulerthlema  12162  prmdiv  12167  prmdiveq  12168  phisum  12172  odzval  12173  odzcllem  12174  odzdvds  12177  reumodprminv  12185  pythagtriplem3  12199  pythagtriplem18  12213  pythagtriplem19  12214  pclem0  12218  pclemub  12219  pclemdc  12220  pcprecl  12221  pcprendvds  12222  pcpremul  12225  pceulem  12226  pceu  12227  pczpre  12229  pcdiv  12234  pcqmul  12235  pcqcl  12238  pcexp  12241  pcxnn0cl  12242  pcxcl  12243  pcge0  12244  pcdvdsb  12251  pcneg  12256  pcabs  12257  pcgcd1  12259  pc2dvds  12261  pc11  12262  pcz  12263  pcprmpw2  12264  pcprmpw  12265  dvdsprmpweq  12266  dvdsprmpweqnn  12267  dvdsprmpweqle  12268  pcaddlem  12270  pcadd  12271  pcfac  12280  oddprmdvds  12284  prmpwdvds  12285  pockthi  12288  infpnlem2  12290  1arithlem1  12293  ennnfonelemnn0  12355  ennnfonelemr  12356  mgm1  12601  mgmidmo  12603  mgmlrid  12610  lidrideqd  12612  lidrididd  12613  grprinvlem  12616  grprinvd  12617  txdis1cn  12918  cnmptcom  12938  psmettri2  12968  isxmet2d  12988  xmeteq0  12999  xmettri2  13001  elblps  13030  elbl  13031  blssps  13067  blss  13068  ssblex  13071  blin2  13072  metss2  13138  comet  13139  bdmopn  13144  txmetcnp  13158  blssioo  13185  divcnap  13195  cncfval  13199  cncfi  13205  mulc1cncf  13216  cdivcncfap  13227  mulcncf  13231  expcncf  13232  cnopnap  13234  ellimc3apf  13269  cnlimci  13282  limccnpcntop  13284  limccnp2lem  13285  reldvg  13288  eldvap  13291  dvexp  13315  dvexp2  13316  dvrecap  13317  sin0pilem2  13343  relogbcxpbap  13523  logbgcd1irr  13525  2irrexpq  13534  2irrexpqap  13536  lgsneg  13565  lgsdilem  13568  lgsdir  13576  lgsdilem2  13577  lgsdi  13578  lgsne0  13579  lgsdirnn0  13588  lgsdinn0  13589  2sqlem6  13596  2sqlem8  13599  2sqlem9  13600  2sqlem10  13601  trilpolemclim  13915  trilpolemcl  13916  trilpolemisumle  13917  trilpolemeq1  13919  trilpolemlt1  13920  trilpo  13922  trirec0  13923  redcwlpo  13934  nconstwlpolemgt0  13942  nconstwlpo  13944  neapmkv  13946