Theorem oveq2 5952

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

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

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 4045  df-iota 5232  df-fv 5279  df-ov 5947

This theorem is referenced by:  oveq12  5953  oveq2i  5955  oveq2d  5960  ovanraleqv  5968  ovrspc2v  5970  oveqrspc2v  5971  rspceov  5987  fovcld  6050  ovmpos  6069  ov2gf  6070  ovi3  6083  caovclg  6099  caovcomg  6102  caovassg  6105  caovcang  6108  caovcan  6111  caovordig  6112  caovordg  6114  caovord  6118  caovdig  6121  caovdirg  6124  caovimo  6140  suppssov1  6155  off  6171  caofid0l  6185  caofid2  6188  caofdig  6192  omv  6541  oeiv  6542  oasuc  6550  oawordriexmid  6556  omsuc  6558  nna0r  6564  nnm0r  6565  nnacl  6566  nnmcl  6567  nnacom  6570  nnaass  6571  nndi  6572  nnmass  6573  nnmsucr  6574  nnmcom  6575  nnaordi  6594  nnaord  6595  nnmordi  6602  nnmord  6603  nnaordex  6614  nnawordex  6615  nnm00  6616  eroveu  6713  ecopovtrn  6719  ecopovtrng  6722  th3qlem2  6725  th3q  6727  ecovcom  6729  ecovicom  6730  ecovass  6731  ecoviass  6732  ecovdi  6733  ecovidi  6734  exmidpw2en  7009  acneq  7314  addcanpig  7447  mulcanpig  7448  addcmpblnq  7480  addclnq  7488  mulclnq  7489  recexnq  7503  recmulnqg  7504  ltanqg  7513  ltmnqg  7514  ltexnqq  7521  enq0ref  7546  enq0tr  7547  addcmpblnq0  7556  mulnnnq0  7563  addclnq0  7564  mulclnq0  7565  distrnq0  7572  mulcomnq0  7573  addassnq0  7575  nq02m  7578  prarloclem3  7610  genipv  7622  genpassl  7637  genpassu  7638  addlocpr  7649  distrlem1prl  7695  distrlem1pru  7696  1idprl  7703  1idpru  7704  ltexprlemell  7711  ltexprlemelu  7712  ltexpri  7726  lteupri  7730  ltaprlem  7731  recexprlem1ssl  7746  recexprlem1ssu  7747  recexpr  7751  cauappcvgprlemm  7758  cauappcvgprlemdisj  7764  cauappcvgprlemloc  7765  cauappcvgprlemladdru  7769  cauappcvgprlemladdrl  7770  cauappcvgprlem1  7772  cauappcvgprlemlim  7774  cauappcvgpr  7775  mulcmpblnrlemg  7853  addclsr  7866  mulclsr  7867  ltasrg  7883  negexsr  7885  recexgt0sr  7886  mulgt0sr  7891  mulextsr1  7894  srpospr  7896  caucvgsrlemgt1  7908  map2psrprg  7918  axaddrcl  7978  axmulrcl  7980  axaddcom  7983  axrnegex  7992  axprecex  7993  axcnre  7994  axpre-ltadd  7999  axpre-mulgt0  8000  axpre-mulext  8001  rereceu  8002  recriota  8003  axcaucvglemres  8012  readdcan  8212  cnegexlem1  8247  cnegex  8250  addcan  8252  negeq  8265  subadd  8275  addid0  8445  ine0  8466  rimul  8658  cru  8675  apreim  8676  recexap  8726  mulcanapd  8734  receuap  8742  divmulap  8748  rerecapb  8916  cju  9034  nnaddcl  9056  nnmulcl  9057  nnsub  9075  nnnn0addcl  9325  zaddcllempos  9409  zaddcl  9412  zdiv  9461  deceq1  9508  deceq2  9509  uzaddcl  9707  zq  9747  qreccl  9763  cnref1o  9772  xaddnemnf  9979  xaddnepnf  9980  xaddcom  9983  xnn0xadd0  9989  xnegdi  9990  xaddass  9991  xlt2add  10002  xlesubadd  10005  xleaddadd  10009  fzsuc2  10201  fzrevral  10227  fzshftral  10230  2ffzeq  10263  exfzdc  10369  exbtwnzlemshrink  10391  rebtwn2zlemshrink  10396  modqval  10469  modqmuladd  10511  modqmuladdnn0  10513  frecuzrdgrrn  10553  frec2uzrdg  10554  frecuzrdgrcl  10555  frecuzrdgsuc  10559  frecuzrdgrclt  10560  frecuzrdgg  10561  frecuzrdgsuctlem  10568  frecfzennn  10571  uzsinds  10589  iseqvalcbv  10604  seq3val  10605  seqvalcd  10606  seqovcd  10612  seq3caopr3  10636  seq3caopr2  10638  seqcaopr2g  10639  seq3f1olemp  10660  seqf1og  10666  seq3id  10670  seq3homo  10672  seq3z  10673  seqhomog  10675  seqfeq4g  10676  seq3distr  10677  expp1  10691  expnegap0  10692  expcllem  10695  expcl2lemap  10696  m1expcl2  10706  expap0  10714  mulexp  10723  expadd  10726  expmul  10729  leexp2r  10738  leexp1a  10739  bernneq  10805  expnbnd  10808  modqexp  10811  nn0ltexp2  10854  expcan  10861  apexp1  10863  facdiv  10883  faclbnd3  10888  faclbnd6  10889  bcval  10894  bcpasc  10911  bccl  10912  fz1eqb  10935  omgadd  10947  hashunlem  10949  hashfzo  10967  hashfzp1  10969  iswrdinn0  10999  wrdnval  11024  eqwrd  11034  eqs1  11082  shftfvalg  11129  shftfval  11132  cjth  11157  remim  11171  reim0b  11173  cjexp  11204  cnrecnv  11221  cvg1nlemcau  11295  cvg1nlemres  11296  recvguniq  11306  resqrexlemp1rp  11317  resqrexlemfp1  11320  resqrexlemlo  11324  resqrexlemgt0  11331  resqrexlemoverl  11332  resqrexlemglsq  11333  resqrexlemsqa  11335  resqrexlemex  11336  resqrex  11337  absexp  11390  recan  11420  climcn2  11620  subcn2  11622  summodc  11694  fsum3  11698  fsum3cvg3  11707  fsumrev  11754  fisum0diag2  11758  telfsumo  11777  fsumrelem  11782  binomlem  11794  binom  11795  binom1dif  11798  bcxmaslem1  11799  bcxmas  11800  isumshft  11801  divcnv  11808  arisum  11809  trireciplem  11811  expcnvap0  11813  expcnvre  11814  expcnv  11815  explecnv  11816  geosergap  11817  geolim  11822  geolim2  11823  geo2sum  11825  geo2lim  11827  geoisum  11828  geoisumr  11829  geoisum1  11830  geoisum1c  11831  cvgratnnlemsumlt  11839  cvgratz  11843  prodmodc  11889  fprodseq  11894  fprodcl2lem  11916  fprodfac  11926  fprodabs  11927  fprodrev  11930  eftvalcn  11968  efcvgfsum  11978  ege2le3  11982  efcj  11984  efaddlem  11985  efexp  11993  eftlub  12001  efgt1p2  12006  eflegeo  12012  sinval  12013  cosval  12014  demoivreALT  12085  divides  12100  dvdscmul  12129  dvds2ln  12135  dvdstr  12139  odd2np1lem  12183  odd2np1  12184  2tp1odd  12195  opeo  12208  omeo  12209  m1expe  12210  m1expo  12211  m1exp1  12212  divalglemnn  12229  divalglemeunn  12232  divalglemeuneg  12234  divalgmod  12238  ndvdssub  12241  bitsval  12254  bitsfzolem  12265  bitsinv1lem  12272  bitsinv1  12273  gcd0id  12300  bezoutlemnewy  12317  bezoutlema  12320  bezoutlemb  12321  bezoutlemex  12322  bezoutlemaz  12324  bezoutlembz  12325  gcdmultiple  12341  gcdmultiplez  12342  dvdsmulgcd  12346  rplpwr  12348  nn0seqcvgd  12363  dvdslcm  12391  lcmeq0  12393  lcmcl  12394  lcmneg  12396  lcmgcdlem  12399  lcmdvds  12401  lcmid  12402  lcmgcdeq  12405  coprmdvds  12414  mulgcddvds  12416  qredeq  12418  cncongr1  12425  cncongr2  12426  cncongrcoprm  12428  prmind2  12442  isprm6  12469  prmdvdsexp  12470  prmdvdsexpr  12472  sqrt2irr  12484  pw2dvdslemn  12487  pw2dvdseu  12490  oddpwdclemxy  12491  sqpweven  12497  2sqpwodd  12498  sqne2sq  12499  nn0gcdsq  12522  qden1elz  12527  phival  12535  dfphi2  12542  eulerthlemrprm  12551  eulerthlema  12552  prmdiv  12557  prmdiveq  12558  phisum  12563  odzval  12564  odzcllem  12565  odzdvds  12568  reumodprminv  12576  pythagtriplem3  12590  pythagtriplem18  12604  pythagtriplem19  12605  pclem0  12609  pclemub  12610  pclemdc  12611  pcprecl  12612  pcprendvds  12613  pcpremul  12616  pceulem  12617  pceu  12618  pczpre  12620  pcdiv  12625  pcqmul  12626  pcqcl  12629  pcexp  12632  pcxnn0cl  12633  pcxcl  12634  pcge0  12636  pcdvdsb  12643  pcneg  12648  pcabs  12649  pcgcd1  12651  pc2dvds  12653  pc11  12654  pcz  12655  pcprmpw2  12656  pcprmpw  12657  dvdsprmpweq  12658  dvdsprmpweqnn  12659  dvdsprmpweqle  12660  pcaddlem  12662  pcadd  12663  pcfac  12673  oddprmdvds  12677  prmpwdvds  12678  pockthi  12681  infpnlem2  12683  1arithlem1  12686  4sqlemffi  12719  4sqlem12  12725  2expltfac  12762  ennnfonelemnn0  12793  ennnfonelemr  12794  f1ovscpbl  13144  imasaddvallemg  13147  ercpbl  13163  mgm1  13202  mgmidmo  13204  mgmlrid  13211  lidrideqd  13213  lidrididd  13214  grpinvalem  13217  grpinva  13218  gsumfzval  13223  gsumval2  13229  isnsgrp  13238  sgrpass  13240  sgrp1  13243  mndinvmod  13277  imasmnd2  13284  mnd1  13287  mnd1id  13288  mhmpropd  13298  mhmlin  13299  insubm  13317  mhmima  13323  gsumwsubmcl  13328  gsumwmhm  13330  grpinvex  13342  grppropd  13349  dfgrp2  13359  grpidd2  13373  grpinvval  13375  grpinvid1  13384  grplrinv  13389  grpidinv2  13390  grpidinv  13391  grplcan  13394  grpidssd  13408  grpinvssd  13409  dfgrp3mlem  13430  dfgrp3m  13431  grplactcnv  13434  grp1  13438  imasgrp2  13446  mhmlem  13450  mulgnn0gsum  13464  mulginvcom  13483  mulgnn0ass  13494  mulgmodid  13497  issubg  13509  issubg2m  13525  issubg4m  13529  isnsg2  13539  nsgbi  13540  isnsg3  13543  elnmz  13544  nmzbi  13545  ghmlin  13584  ghmrn  13593  ghmnsgima  13604  conjghm  13612  conjnmz  13615  gsumfzconst  13677  rngdi  13702  rngdir  13703  srglz  13747  srgisid  13748  srglmhm  13755  ringid  13788  ringinvnz1ne0  13811  ringinvnzdiv  13812  ring1  13821  ringlghm  13823  imasring  13826  dvdsrtr  13863  lringuplu  13958  issubrng  13961  issubrng2  13972  issubrg  13983  issubrg2  14003  rrgeq0i  14026  rrgeq0  14027  unitrrg  14029  domneq0  14034  lmodlema  14054  islmodd  14055  rmodislmodlem  14112  rmodislmod  14113  lssclg  14126  lss1d  14145  rnglidlmcl  14242  quscrng  14295  cnfldexp  14339  gsumfzfsumlemm  14349  cnfldui  14351  expghmap  14369  zrhval  14379  zrhvalg  14380  znunit  14421  txdis1cn  14750  cnmptcom  14770  psmettri2  14800  isxmet2d  14820  xmeteq0  14831  xmettri2  14833  elblps  14862  elbl  14863  blssps  14899  blss  14900  ssblex  14903  blin2  14904  metss2  14970  comet  14971  bdmopn  14976  txmetcnp  14990  blssioo  15025  divcnap  15037  mpomulcn  15038  expcn  15041  cncfval  15044  cncfi  15050  mulc1cncf  15061  cdivcncfap  15076  mulcncf  15080  expcncf  15081  cnopnap  15083  ellimc3apf  15132  cnlimci  15145  limccnpcntop  15147  limccnp2lem  15148  reldvg  15151  eldvap  15154  dvexp  15183  dvexp2  15184  dvrecap  15185  elplyr  15212  elplyd  15213  ply1termlem  15214  plymullem1  15220  plyadd  15223  plymul  15224  plycoeid3  15229  plycolemc  15230  plyco  15231  plycj  15233  dvply1  15237  dvply2g  15238  sin0pilem2  15254  rpcxpmul2  15385  relogbcxpbap  15437  logbgcd1irr  15439  2irrexpq  15448  2irrexpqap  15450  dvdsppwf1o  15461  mpodvdsmulf1o  15462  fsumdvdsmul  15463  sgmppw  15464  1sgmprm  15466  perfect  15473  lgsneg  15501  lgsdilem  15504  lgsdir  15512  lgsdilem2  15513  lgsdi  15514  lgsne0  15515  lgsdirnn0  15524  lgsdinn0  15525  gausslemma2dlem4  15541  lgseisenlem2  15548  lgseisenlem3  15549  lgseisenlem4  15550  lgsquadlem1  15554  lgsquadlem2  15555  lgsquad2lem2  15559  2lgs  15581  2sqlem6  15597  2sqlem8  15600  2sqlem9  15601  2sqlem10  15602  trilpolemclim  15975  trilpolemcl  15976  trilpolemisumle  15977  trilpolemeq1  15979  trilpolemlt1  15980  trilpo  15982  trirec0  15983  redcwlpo  15994  nconstwlpolemgt0  16003  nconstwlpo  16005  neapmkv  16007