Theorem oveq2 5954

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 3820	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
2	1	fveq2d 5582	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘⟨𝐶, 𝐴⟩) = (𝐹‘⟨𝐶, 𝐵⟩))
3		df-ov 5949	. 2 ⊢ (𝐶𝐹𝐴) = (𝐹‘⟨𝐶, 𝐴⟩)
4		df-ov 5949	. 2 ⊢ (𝐶𝐹𝐵) = (𝐹‘⟨𝐶, 𝐵⟩)
5	2, 3, 4	3eqtr4g 2263	1 ⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))

Syntax hints:   → wi 4   = wceq 1373  ⟨cop 3636  ‘cfv 5272  (class class class)co 5946

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4046  df-iota 5233  df-fv 5280  df-ov 5949

This theorem is referenced by:  oveq12  5955  oveq2i  5957  oveq2d  5962  ovanraleqv  5970  ovrspc2v  5972  oveqrspc2v  5973  rspceov  5989  fovcld  6052  ovmpos  6071  ov2gf  6072  ovi3  6085  caovclg  6101  caovcomg  6104  caovassg  6107  caovcang  6110  caovcan  6113  caovordig  6114  caovordg  6116  caovord  6120  caovdig  6123  caovdirg  6126  caovimo  6142  suppssov1  6157  off  6173  caofid0l  6187  caofid2  6190  caofdig  6194  omv  6543  oeiv  6544  oasuc  6552  oawordriexmid  6558  omsuc  6560  nna0r  6566  nnm0r  6567  nnacl  6568  nnmcl  6569  nnacom  6572  nnaass  6573  nndi  6574  nnmass  6575  nnmsucr  6576  nnmcom  6577  nnaordi  6596  nnaord  6597  nnmordi  6604  nnmord  6605  nnaordex  6616  nnawordex  6617  nnm00  6618  eroveu  6715  ecopovtrn  6721  ecopovtrng  6724  th3qlem2  6727  th3q  6729  ecovcom  6731  ecovicom  6732  ecovass  6733  ecoviass  6734  ecovdi  6735  ecovidi  6736  exmidpw2en  7011  acneq  7316  addcanpig  7449  mulcanpig  7450  addcmpblnq  7482  addclnq  7490  mulclnq  7491  recexnq  7505  recmulnqg  7506  ltanqg  7515  ltmnqg  7516  ltexnqq  7523  enq0ref  7548  enq0tr  7549  addcmpblnq0  7558  mulnnnq0  7565  addclnq0  7566  mulclnq0  7567  distrnq0  7574  mulcomnq0  7575  addassnq0  7577  nq02m  7580  prarloclem3  7612  genipv  7624  genpassl  7639  genpassu  7640  addlocpr  7651  distrlem1prl  7697  distrlem1pru  7698  1idprl  7705  1idpru  7706  ltexprlemell  7713  ltexprlemelu  7714  ltexpri  7728  lteupri  7732  ltaprlem  7733  recexprlem1ssl  7748  recexprlem1ssu  7749  recexpr  7753  cauappcvgprlemm  7760  cauappcvgprlemdisj  7766  cauappcvgprlemloc  7767  cauappcvgprlemladdru  7771  cauappcvgprlemladdrl  7772  cauappcvgprlem1  7774  cauappcvgprlemlim  7776  cauappcvgpr  7777  mulcmpblnrlemg  7855  addclsr  7868  mulclsr  7869  ltasrg  7885  negexsr  7887  recexgt0sr  7888  mulgt0sr  7893  mulextsr1  7896  srpospr  7898  caucvgsrlemgt1  7910  map2psrprg  7920  axaddrcl  7980  axmulrcl  7982  axaddcom  7985  axrnegex  7994  axprecex  7995  axcnre  7996  axpre-ltadd  8001  axpre-mulgt0  8002  axpre-mulext  8003  rereceu  8004  recriota  8005  axcaucvglemres  8014  readdcan  8214  cnegexlem1  8249  cnegex  8252  addcan  8254  negeq  8267  subadd  8277  addid0  8447  ine0  8468  rimul  8660  cru  8677  apreim  8678  recexap  8728  mulcanapd  8736  receuap  8744  divmulap  8750  rerecapb  8918  cju  9036  nnaddcl  9058  nnmulcl  9059  nnsub  9077  nnnn0addcl  9327  zaddcllempos  9411  zaddcl  9414  zdiv  9463  deceq1  9510  deceq2  9511  uzaddcl  9709  zq  9749  qreccl  9765  cnref1o  9774  xaddnemnf  9981  xaddnepnf  9982  xaddcom  9985  xnn0xadd0  9991  xnegdi  9992  xaddass  9993  xlt2add  10004  xlesubadd  10007  xleaddadd  10011  fzsuc2  10203  fzrevral  10229  fzshftral  10232  2ffzeq  10265  exfzdc  10371  exbtwnzlemshrink  10393  rebtwn2zlemshrink  10398  modqval  10471  modqmuladd  10513  modqmuladdnn0  10515  frecuzrdgrrn  10555  frec2uzrdg  10556  frecuzrdgrcl  10557  frecuzrdgsuc  10561  frecuzrdgrclt  10562  frecuzrdgg  10563  frecuzrdgsuctlem  10570  frecfzennn  10573  uzsinds  10591  iseqvalcbv  10606  seq3val  10607  seqvalcd  10608  seqovcd  10614  seq3caopr3  10638  seq3caopr2  10640  seqcaopr2g  10641  seq3f1olemp  10662  seqf1og  10668  seq3id  10672  seq3homo  10674  seq3z  10675  seqhomog  10677  seqfeq4g  10678  seq3distr  10679  expp1  10693  expnegap0  10694  expcllem  10697  expcl2lemap  10698  m1expcl2  10708  expap0  10716  mulexp  10725  expadd  10728  expmul  10731  leexp2r  10740  leexp1a  10741  bernneq  10807  expnbnd  10810  modqexp  10813  nn0ltexp2  10856  expcan  10863  apexp1  10865  facdiv  10885  faclbnd3  10890  faclbnd6  10891  bcval  10896  bcpasc  10913  bccl  10914  fz1eqb  10937  omgadd  10949  hashunlem  10951  hashfzo  10969  hashfzp1  10971  iswrdinn0  11001  wrdnval  11026  eqwrd  11036  eqs1  11085  pfxeq  11150  shftfvalg  11162  shftfval  11165  cjth  11190  remim  11204  reim0b  11206  cjexp  11237  cnrecnv  11254  cvg1nlemcau  11328  cvg1nlemres  11329  recvguniq  11339  resqrexlemp1rp  11350  resqrexlemfp1  11353  resqrexlemlo  11357  resqrexlemgt0  11364  resqrexlemoverl  11365  resqrexlemglsq  11366  resqrexlemsqa  11368  resqrexlemex  11369  resqrex  11370  absexp  11423  recan  11453  climcn2  11653  subcn2  11655  summodc  11727  fsum3  11731  fsum3cvg3  11740  fsumrev  11787  fisum0diag2  11791  telfsumo  11810  fsumrelem  11815  binomlem  11827  binom  11828  binom1dif  11831  bcxmaslem1  11832  bcxmas  11833  isumshft  11834  divcnv  11841  arisum  11842  trireciplem  11844  expcnvap0  11846  expcnvre  11847  expcnv  11848  explecnv  11849  geosergap  11850  geolim  11855  geolim2  11856  geo2sum  11858  geo2lim  11860  geoisum  11861  geoisumr  11862  geoisum1  11863  geoisum1c  11864  cvgratnnlemsumlt  11872  cvgratz  11876  prodmodc  11922  fprodseq  11927  fprodcl2lem  11949  fprodfac  11959  fprodabs  11960  fprodrev  11963  eftvalcn  12001  efcvgfsum  12011  ege2le3  12015  efcj  12017  efaddlem  12018  efexp  12026  eftlub  12034  efgt1p2  12039  eflegeo  12045  sinval  12046  cosval  12047  demoivreALT  12118  divides  12133  dvdscmul  12162  dvds2ln  12168  dvdstr  12172  odd2np1lem  12216  odd2np1  12217  2tp1odd  12228  opeo  12241  omeo  12242  m1expe  12243  m1expo  12244  m1exp1  12245  divalglemnn  12262  divalglemeunn  12265  divalglemeuneg  12267  divalgmod  12271  ndvdssub  12274  bitsval  12287  bitsfzolem  12298  bitsinv1lem  12305  bitsinv1  12306  gcd0id  12333  bezoutlemnewy  12350  bezoutlema  12353  bezoutlemb  12354  bezoutlemex  12355  bezoutlemaz  12357  bezoutlembz  12358  gcdmultiple  12374  gcdmultiplez  12375  dvdsmulgcd  12379  rplpwr  12381  nn0seqcvgd  12396  dvdslcm  12424  lcmeq0  12426  lcmcl  12427  lcmneg  12429  lcmgcdlem  12432  lcmdvds  12434  lcmid  12435  lcmgcdeq  12438  coprmdvds  12447  mulgcddvds  12449  qredeq  12451  cncongr1  12458  cncongr2  12459  cncongrcoprm  12461  prmind2  12475  isprm6  12502  prmdvdsexp  12503  prmdvdsexpr  12505  sqrt2irr  12517  pw2dvdslemn  12520  pw2dvdseu  12523  oddpwdclemxy  12524  sqpweven  12530  2sqpwodd  12531  sqne2sq  12532  nn0gcdsq  12555  qden1elz  12560  phival  12568  dfphi2  12575  eulerthlemrprm  12584  eulerthlema  12585  prmdiv  12590  prmdiveq  12591  phisum  12596  odzval  12597  odzcllem  12598  odzdvds  12601  reumodprminv  12609  pythagtriplem3  12623  pythagtriplem18  12637  pythagtriplem19  12638  pclem0  12642  pclemub  12643  pclemdc  12644  pcprecl  12645  pcprendvds  12646  pcpremul  12649  pceulem  12650  pceu  12651  pczpre  12653  pcdiv  12658  pcqmul  12659  pcqcl  12662  pcexp  12665  pcxnn0cl  12666  pcxcl  12667  pcge0  12669  pcdvdsb  12676  pcneg  12681  pcabs  12682  pcgcd1  12684  pc2dvds  12686  pc11  12687  pcz  12688  pcprmpw2  12689  pcprmpw  12690  dvdsprmpweq  12691  dvdsprmpweqnn  12692  dvdsprmpweqle  12693  pcaddlem  12695  pcadd  12696  pcfac  12706  oddprmdvds  12710  prmpwdvds  12711  pockthi  12714  infpnlem2  12716  1arithlem1  12719  4sqlemffi  12752  4sqlem12  12758  2expltfac  12795  ennnfonelemnn0  12826  ennnfonelemr  12827  f1ovscpbl  13177  imasaddvallemg  13180  ercpbl  13196  mgm1  13235  mgmidmo  13237  mgmlrid  13244  lidrideqd  13246  lidrididd  13247  grpinvalem  13250  grpinva  13251  gsumfzval  13256  gsumval2  13262  isnsgrp  13271  sgrpass  13273  sgrp1  13276  mndinvmod  13310  imasmnd2  13317  mnd1  13320  mnd1id  13321  mhmpropd  13331  mhmlin  13332  insubm  13350  mhmima  13356  gsumwsubmcl  13361  gsumwmhm  13363  grpinvex  13375  grppropd  13382  dfgrp2  13392  grpidd2  13406  grpinvval  13408  grpinvid1  13417  grplrinv  13422  grpidinv2  13423  grpidinv  13424  grplcan  13427  grpidssd  13441  grpinvssd  13442  dfgrp3mlem  13463  dfgrp3m  13464  grplactcnv  13467  grp1  13471  imasgrp2  13479  mhmlem  13483  mulgnn0gsum  13497  mulginvcom  13516  mulgnn0ass  13527  mulgmodid  13530  issubg  13542  issubg2m  13558  issubg4m  13562  isnsg2  13572  nsgbi  13573  isnsg3  13576  elnmz  13577  nmzbi  13578  ghmlin  13617  ghmrn  13626  ghmnsgima  13637  conjghm  13645  conjnmz  13648  gsumfzconst  13710  rngdi  13735  rngdir  13736  srglz  13780  srgisid  13781  srglmhm  13788  ringid  13821  ringinvnz1ne0  13844  ringinvnzdiv  13845  ring1  13854  ringlghm  13856  imasring  13859  dvdsrtr  13896  lringuplu  13991  issubrng  13994  issubrng2  14005  issubrg  14016  issubrg2  14036  rrgeq0i  14059  rrgeq0  14060  unitrrg  14062  domneq0  14067  lmodlema  14087  islmodd  14088  rmodislmodlem  14145  rmodislmod  14146  lssclg  14159  lss1d  14178  rnglidlmcl  14275  quscrng  14328  cnfldexp  14372  gsumfzfsumlemm  14382  cnfldui  14384  expghmap  14402  zrhval  14412  zrhvalg  14413  znunit  14454  txdis1cn  14783  cnmptcom  14803  psmettri2  14833  isxmet2d  14853  xmeteq0  14864  xmettri2  14866  elblps  14895  elbl  14896  blssps  14932  blss  14933  ssblex  14936  blin2  14937  metss2  15003  comet  15004  bdmopn  15009  txmetcnp  15023  blssioo  15058  divcnap  15070  mpomulcn  15071  expcn  15074  cncfval  15077  cncfi  15083  mulc1cncf  15094  cdivcncfap  15109  mulcncf  15113  expcncf  15114  cnopnap  15116  ellimc3apf  15165  cnlimci  15178  limccnpcntop  15180  limccnp2lem  15181  reldvg  15184  eldvap  15187  dvexp  15216  dvexp2  15217  dvrecap  15218  elplyr  15245  elplyd  15246  ply1termlem  15247  plymullem1  15253  plyadd  15256  plymul  15257  plycoeid3  15262  plycolemc  15263  plyco  15264  plycj  15266  dvply1  15270  dvply2g  15271  sin0pilem2  15287  rpcxpmul2  15418  relogbcxpbap  15470  logbgcd1irr  15472  2irrexpq  15481  2irrexpqap  15483  dvdsppwf1o  15494  mpodvdsmulf1o  15495  fsumdvdsmul  15496  sgmppw  15497  1sgmprm  15499  perfect  15506  lgsneg  15534  lgsdilem  15537  lgsdir  15545  lgsdilem2  15546  lgsdi  15547  lgsne0  15548  lgsdirnn0  15557  lgsdinn0  15558  gausslemma2dlem4  15574  lgseisenlem2  15581  lgseisenlem3  15582  lgseisenlem4  15583  lgsquadlem1  15587  lgsquadlem2  15588  lgsquad2lem2  15592  2lgs  15614  2sqlem6  15630  2sqlem8  15633  2sqlem9  15634  2sqlem10  15635  trilpolemclim  16012  trilpolemcl  16013  trilpolemisumle  16014  trilpolemeq1  16016  trilpolemlt1  16017  trilpo  16019  trirec0  16020  redcwlpo  16031  nconstwlpolemgt0  16040  nconstwlpo  16042  neapmkv  16044