Theorem oveq2 6021

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 3861	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
2	1	fveq2d 5639	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘⟨𝐶, 𝐴⟩) = (𝐹‘⟨𝐶, 𝐵⟩))
3		df-ov 6016	. 2 ⊢ (𝐶𝐹𝐴) = (𝐹‘⟨𝐶, 𝐴⟩)
4		df-ov 6016	. 2 ⊢ (𝐶𝐹𝐵) = (𝐹‘⟨𝐶, 𝐵⟩)
5	2, 3, 4	3eqtr4g 2287	1 ⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))

Syntax hints:   → wi 4   = wceq 1395  ⟨cop 3670  ‘cfv 5324  (class class class)co 6013

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-iota 5284  df-fv 5332  df-ov 6016

This theorem is referenced by:  oveq12  6022  oveq2i  6024  oveq2d  6029  ovanraleqv  6037  ovrspc2v  6039  oveqrspc2v  6040  rspceov  6056  fovcld  6121  ovmpos  6140  ov2gf  6141  ovi3  6154  caovclg  6170  caovcomg  6173  caovassg  6176  caovcang  6179  caovcan  6182  caovordig  6183  caovordg  6185  caovord  6189  caovdig  6192  caovdirg  6195  caovimo  6211  suppssov1  6227  off  6243  caofid0l  6257  caofid2  6260  caofdig  6264  omv  6618  oeiv  6619  oasuc  6627  oawordriexmid  6633  omsuc  6635  nna0r  6641  nnm0r  6642  nnacl  6643  nnmcl  6644  nnacom  6647  nnaass  6648  nndi  6649  nnmass  6650  nnmsucr  6651  nnmcom  6652  nnaordi  6671  nnaord  6672  nnmordi  6679  nnmord  6680  nnaordex  6691  nnawordex  6692  nnm00  6693  eroveu  6790  ecopovtrn  6796  ecopovtrng  6799  th3qlem2  6802  th3q  6804  ecovcom  6806  ecovicom  6807  ecovass  6808  ecoviass  6809  ecovdi  6810  ecovidi  6811  exmidpw2en  7097  acneq  7407  addcanpig  7544  mulcanpig  7545  addcmpblnq  7577  addclnq  7585  mulclnq  7586  recexnq  7600  recmulnqg  7601  ltanqg  7610  ltmnqg  7611  ltexnqq  7618  enq0ref  7643  enq0tr  7644  addcmpblnq0  7653  mulnnnq0  7660  addclnq0  7661  mulclnq0  7662  distrnq0  7669  mulcomnq0  7670  addassnq0  7672  nq02m  7675  prarloclem3  7707  genipv  7719  genpassl  7734  genpassu  7735  addlocpr  7746  distrlem1prl  7792  distrlem1pru  7793  1idprl  7800  1idpru  7801  ltexprlemell  7808  ltexprlemelu  7809  ltexpri  7823  lteupri  7827  ltaprlem  7828  recexprlem1ssl  7843  recexprlem1ssu  7844  recexpr  7848  cauappcvgprlemm  7855  cauappcvgprlemdisj  7861  cauappcvgprlemloc  7862  cauappcvgprlemladdru  7866  cauappcvgprlemladdrl  7867  cauappcvgprlem1  7869  cauappcvgprlemlim  7871  cauappcvgpr  7872  mulcmpblnrlemg  7950  addclsr  7963  mulclsr  7964  ltasrg  7980  negexsr  7982  recexgt0sr  7983  mulgt0sr  7988  mulextsr1  7991  srpospr  7993  caucvgsrlemgt1  8005  map2psrprg  8015  axaddrcl  8075  axmulrcl  8077  axaddcom  8080  axrnegex  8089  axprecex  8090  axcnre  8091  axpre-ltadd  8096  axpre-mulgt0  8097  axpre-mulext  8098  rereceu  8099  recriota  8100  axcaucvglemres  8109  readdcan  8309  cnegexlem1  8344  cnegex  8347  addcan  8349  negeq  8362  subadd  8372  addid0  8542  ine0  8563  rimul  8755  cru  8772  apreim  8773  recexap  8823  mulcanapd  8831  receuap  8839  divmulap  8845  rerecapb  9013  cju  9131  nnaddcl  9153  nnmulcl  9154  nnsub  9172  nnnn0addcl  9422  zaddcllempos  9506  zaddcl  9509  zdiv  9558  deceq1  9605  deceq2  9606  uzaddcl  9810  zq  9850  qreccl  9866  cnref1o  9875  xaddnemnf  10082  xaddnepnf  10083  xaddcom  10086  xnn0xadd0  10092  xnegdi  10093  xaddass  10094  xlt2add  10105  xlesubadd  10108  xleaddadd  10112  fzsuc2  10304  fzrevral  10330  fzshftral  10333  2ffzeq  10366  exfzdc  10476  exbtwnzlemshrink  10498  rebtwn2zlemshrink  10503  modqval  10576  modqmuladd  10618  modqmuladdnn0  10620  frecuzrdgrrn  10660  frec2uzrdg  10661  frecuzrdgrcl  10662  frecuzrdgsuc  10666  frecuzrdgrclt  10667  frecuzrdgg  10668  frecuzrdgsuctlem  10675  frecfzennn  10678  uzsinds  10696  iseqvalcbv  10711  seq3val  10712  seqvalcd  10713  seqovcd  10719  seq3caopr3  10743  seq3caopr2  10745  seqcaopr2g  10746  seq3f1olemp  10767  seqf1og  10773  seq3id  10777  seq3homo  10779  seq3z  10780  seqhomog  10782  seqfeq4g  10783  seq3distr  10784  expp1  10798  expnegap0  10799  expcllem  10802  expcl2lemap  10803  m1expcl2  10813  expap0  10821  mulexp  10830  expadd  10833  expmul  10836  leexp2r  10845  leexp1a  10846  bernneq  10912  expnbnd  10915  modqexp  10918  nn0ltexp2  10961  expcan  10968  apexp1  10970  facdiv  10990  faclbnd3  10995  faclbnd6  10996  bcval  11001  bcpasc  11018  bccl  11019  fz1eqb  11042  omgadd  11055  hashunlem  11057  hashfzo  11076  hashfzp1  11078  iswrdinn0  11108  wrdnval  11134  eqwrd  11144  eqs1  11195  pfxeq  11267  ccatopth  11287  wrd2ind  11294  swrdccatin1  11296  swrdccatin2  11300  pfxccatin12lem2  11302  swrdccat3blem  11310  pfxccatid  11312  swrdccatin1d  11314  swrdccatin2d  11315  s2dmg  11361  shftfvalg  11369  shftfval  11372  cjth  11397  remim  11411  reim0b  11413  cjexp  11444  cnrecnv  11461  cvg1nlemcau  11535  cvg1nlemres  11536  recvguniq  11546  resqrexlemp1rp  11557  resqrexlemfp1  11560  resqrexlemlo  11564  resqrexlemgt0  11571  resqrexlemoverl  11572  resqrexlemglsq  11573  resqrexlemsqa  11575  resqrexlemex  11576  resqrex  11577  absexp  11630  recan  11660  climcn2  11860  subcn2  11862  summodc  11934  fsum3  11938  fsum3cvg3  11947  fsumrev  11994  fisum0diag2  11998  telfsumo  12017  fsumrelem  12022  binomlem  12034  binom  12035  binom1dif  12038  bcxmaslem1  12039  bcxmas  12040  isumshft  12041  divcnv  12048  arisum  12049  trireciplem  12051  expcnvap0  12053  expcnvre  12054  expcnv  12055  explecnv  12056  geosergap  12057  geolim  12062  geolim2  12063  geo2sum  12065  geo2lim  12067  geoisum  12068  geoisumr  12069  geoisum1  12070  geoisum1c  12071  cvgratnnlemsumlt  12079  cvgratz  12083  prodmodc  12129  fprodseq  12134  fprodcl2lem  12156  fprodfac  12166  fprodabs  12167  fprodrev  12170  eftvalcn  12208  efcvgfsum  12218  ege2le3  12222  efcj  12224  efaddlem  12225  efexp  12233  eftlub  12241  efgt1p2  12246  eflegeo  12252  sinval  12253  cosval  12254  demoivreALT  12325  divides  12340  dvdscmul  12369  dvds2ln  12375  dvdstr  12379  odd2np1lem  12423  odd2np1  12424  2tp1odd  12435  opeo  12448  omeo  12449  m1expe  12450  m1expo  12451  m1exp1  12452  divalglemnn  12469  divalglemeunn  12472  divalglemeuneg  12474  divalgmod  12478  ndvdssub  12481  bitsval  12494  bitsfzolem  12505  bitsinv1lem  12512  bitsinv1  12513  gcd0id  12540  bezoutlemnewy  12557  bezoutlema  12560  bezoutlemb  12561  bezoutlemex  12562  bezoutlemaz  12564  bezoutlembz  12565  gcdmultiple  12581  gcdmultiplez  12582  dvdsmulgcd  12586  rplpwr  12588  nn0seqcvgd  12603  dvdslcm  12631  lcmeq0  12633  lcmcl  12634  lcmneg  12636  lcmgcdlem  12639  lcmdvds  12641  lcmid  12642  lcmgcdeq  12645  coprmdvds  12654  mulgcddvds  12656  qredeq  12658  cncongr1  12665  cncongr2  12666  cncongrcoprm  12668  prmind2  12682  isprm6  12709  prmdvdsexp  12710  prmdvdsexpr  12712  sqrt2irr  12724  pw2dvdslemn  12727  pw2dvdseu  12730  oddpwdclemxy  12731  sqpweven  12737  2sqpwodd  12738  sqne2sq  12739  nn0gcdsq  12762  qden1elz  12767  phival  12775  dfphi2  12782  eulerthlemrprm  12791  eulerthlema  12792  prmdiv  12797  prmdiveq  12798  phisum  12803  odzval  12804  odzcllem  12805  odzdvds  12808  reumodprminv  12816  pythagtriplem3  12830  pythagtriplem18  12844  pythagtriplem19  12845  pclem0  12849  pclemub  12850  pclemdc  12851  pcprecl  12852  pcprendvds  12853  pcpremul  12856  pceulem  12857  pceu  12858  pczpre  12860  pcdiv  12865  pcqmul  12866  pcqcl  12869  pcexp  12872  pcxnn0cl  12873  pcxcl  12874  pcge0  12876  pcdvdsb  12883  pcneg  12888  pcabs  12889  pcgcd1  12891  pc2dvds  12893  pc11  12894  pcz  12895  pcprmpw2  12896  pcprmpw  12897  dvdsprmpweq  12898  dvdsprmpweqnn  12899  dvdsprmpweqle  12900  pcaddlem  12902  pcadd  12903  pcfac  12913  oddprmdvds  12917  prmpwdvds  12918  pockthi  12921  infpnlem2  12923  1arithlem1  12926  4sqlemffi  12959  4sqlem12  12965  2expltfac  13002  ennnfonelemnn0  13033  ennnfonelemr  13034  f1ovscpbl  13385  imasaddvallemg  13388  ercpbl  13404  mgm1  13443  mgmidmo  13445  mgmlrid  13452  lidrideqd  13454  lidrididd  13455  grpinvalem  13458  grpinva  13459  gsumfzval  13464  gsumval2  13470  isnsgrp  13479  sgrpass  13481  sgrp1  13484  mndinvmod  13518  imasmnd2  13525  mnd1  13528  mnd1id  13529  mhmpropd  13539  mhmlin  13540  insubm  13558  mhmima  13564  gsumwsubmcl  13569  gsumwmhm  13571  grpinvex  13583  grppropd  13590  dfgrp2  13600  grpidd2  13614  grpinvval  13616  grpinvid1  13625  grplrinv  13630  grpidinv2  13631  grpidinv  13632  grplcan  13635  grpidssd  13649  grpinvssd  13650  dfgrp3mlem  13671  dfgrp3m  13672  grplactcnv  13675  grp1  13679  imasgrp2  13687  mhmlem  13691  mulgnn0gsum  13705  mulginvcom  13724  mulgnn0ass  13735  mulgmodid  13738  issubg  13750  issubg2m  13766  issubg4m  13770  isnsg2  13780  nsgbi  13781  isnsg3  13784  elnmz  13785  nmzbi  13786  ghmlin  13825  ghmrn  13834  ghmnsgima  13845  conjghm  13853  conjnmz  13856  gsumfzconst  13918  rngdi  13943  rngdir  13944  srglz  13988  srgisid  13989  srglmhm  13996  ringid  14029  ringinvnz1ne0  14052  ringinvnzdiv  14053  ring1  14062  ringlghm  14064  imasring  14067  dvdsrtr  14105  lringuplu  14200  issubrng  14203  issubrng2  14214  issubrg  14225  issubrg2  14245  rrgeq0i  14268  rrgeq0  14269  unitrrg  14271  domneq0  14276  lmodlema  14296  islmodd  14297  rmodislmodlem  14354  rmodislmod  14355  lssclg  14368  lss1d  14387  rnglidlmcl  14484  quscrng  14537  cnfldexp  14581  gsumfzfsumlemm  14591  cnfldui  14593  expghmap  14611  zrhval  14621  zrhvalg  14622  znunit  14663  txdis1cn  14992  cnmptcom  15012  psmettri2  15042  isxmet2d  15062  xmeteq0  15073  xmettri2  15075  elblps  15104  elbl  15105  blssps  15141  blss  15142  ssblex  15145  blin2  15146  metss2  15212  comet  15213  bdmopn  15218  txmetcnp  15232  blssioo  15267  divcnap  15279  mpomulcn  15280  expcn  15283  cncfval  15286  cncfi  15292  mulc1cncf  15303  cdivcncfap  15318  mulcncf  15322  expcncf  15323  cnopnap  15325  ellimc3apf  15374  cnlimci  15387  limccnpcntop  15389  limccnp2lem  15390  reldvg  15393  eldvap  15396  dvexp  15425  dvexp2  15426  dvrecap  15427  elplyr  15454  elplyd  15455  ply1termlem  15456  plymullem1  15462  plyadd  15465  plymul  15466  plycoeid3  15471  plycolemc  15472  plyco  15473  plycj  15475  dvply1  15479  dvply2g  15480  sin0pilem2  15496  rpcxpmul2  15627  relogbcxpbap  15679  logbgcd1irr  15681  2irrexpq  15690  2irrexpqap  15692  dvdsppwf1o  15703  mpodvdsmulf1o  15704  fsumdvdsmul  15705  sgmppw  15706  1sgmprm  15708  perfect  15715  lgsneg  15743  lgsdilem  15746  lgsdir  15754  lgsdilem2  15755  lgsdi  15756  lgsne0  15757  lgsdirnn0  15766  lgsdinn0  15767  gausslemma2dlem4  15783  lgseisenlem2  15790  lgseisenlem3  15791  lgseisenlem4  15792  lgsquadlem1  15796  lgsquadlem2  15797  lgsquad2lem2  15801  2lgs  15823  2sqlem6  15839  2sqlem8  15842  2sqlem9  15843  2sqlem10  15844  wlkeq  16151  wlkl1loop  16155  uspgr2wlkeq  16162  upgr2wlkdc  16172  clwwlknonmpo  16223  trilpolemclim  16576  trilpolemcl  16577  trilpolemisumle  16578  trilpolemeq1  16580  trilpolemlt1  16581  trilpo  16583  trirec0  16584  redcwlpo  16595  nconstwlpolemgt0  16604  nconstwlpo  16606  neapmkv  16608