Theorem oveq2 6025

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 3863	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
2	1	fveq2d 5643	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘⟨𝐶, 𝐴⟩) = (𝐹‘⟨𝐶, 𝐵⟩))
3		df-ov 6020	. 2 ⊢ (𝐶𝐹𝐴) = (𝐹‘⟨𝐶, 𝐴⟩)
4		df-ov 6020	. 2 ⊢ (𝐶𝐹𝐵) = (𝐹‘⟨𝐶, 𝐵⟩)
5	2, 3, 4	3eqtr4g 2289	1 ⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))

Syntax hints:   → wi 4   = wceq 1397  ⟨cop 3672  ‘cfv 5326  (class class class)co 6017

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6020

This theorem is referenced by:  oveq12  6026  oveq2i  6028  oveq2d  6033  ovanraleqv  6041  ovrspc2v  6043  oveqrspc2v  6044  rspceov  6060  fovcld  6125  ovmpos  6144  ov2gf  6145  ovi3  6158  caovclg  6174  caovcomg  6177  caovassg  6180  caovcang  6183  caovcan  6186  caovordig  6187  caovordg  6189  caovord  6193  caovdig  6196  caovdirg  6199  caovimo  6215  suppssov1  6231  off  6247  caofid0l  6261  caofid2  6264  caofdig  6268  omv  6622  oeiv  6623  oasuc  6631  oawordriexmid  6637  omsuc  6639  nna0r  6645  nnm0r  6646  nnacl  6647  nnmcl  6648  nnacom  6651  nnaass  6652  nndi  6653  nnmass  6654  nnmsucr  6655  nnmcom  6656  nnaordi  6675  nnaord  6676  nnmordi  6683  nnmord  6684  nnaordex  6695  nnawordex  6696  nnm00  6697  eroveu  6794  ecopovtrn  6800  ecopovtrng  6803  th3qlem2  6806  th3q  6808  ecovcom  6810  ecovicom  6811  ecovass  6812  ecoviass  6813  ecovdi  6814  ecovidi  6815  exmidpw2en  7103  acneq  7416  addcanpig  7553  mulcanpig  7554  addcmpblnq  7586  addclnq  7594  mulclnq  7595  recexnq  7609  recmulnqg  7610  ltanqg  7619  ltmnqg  7620  ltexnqq  7627  enq0ref  7652  enq0tr  7653  addcmpblnq0  7662  mulnnnq0  7669  addclnq0  7670  mulclnq0  7671  distrnq0  7678  mulcomnq0  7679  addassnq0  7681  nq02m  7684  prarloclem3  7716  genipv  7728  genpassl  7743  genpassu  7744  addlocpr  7755  distrlem1prl  7801  distrlem1pru  7802  1idprl  7809  1idpru  7810  ltexprlemell  7817  ltexprlemelu  7818  ltexpri  7832  lteupri  7836  ltaprlem  7837  recexprlem1ssl  7852  recexprlem1ssu  7853  recexpr  7857  cauappcvgprlemm  7864  cauappcvgprlemdisj  7870  cauappcvgprlemloc  7871  cauappcvgprlemladdru  7875  cauappcvgprlemladdrl  7876  cauappcvgprlem1  7878  cauappcvgprlemlim  7880  cauappcvgpr  7881  mulcmpblnrlemg  7959  addclsr  7972  mulclsr  7973  ltasrg  7989  negexsr  7991  recexgt0sr  7992  mulgt0sr  7997  mulextsr1  8000  srpospr  8002  caucvgsrlemgt1  8014  map2psrprg  8024  axaddrcl  8084  axmulrcl  8086  axaddcom  8089  axrnegex  8098  axprecex  8099  axcnre  8100  axpre-ltadd  8105  axpre-mulgt0  8106  axpre-mulext  8107  rereceu  8108  recriota  8109  axcaucvglemres  8118  readdcan  8318  cnegexlem1  8353  cnegex  8356  addcan  8358  negeq  8371  subadd  8381  addid0  8551  ine0  8572  rimul  8764  cru  8781  apreim  8782  recexap  8832  mulcanapd  8840  receuap  8848  divmulap  8854  rerecapb  9022  cju  9140  nnaddcl  9162  nnmulcl  9163  nnsub  9181  nnnn0addcl  9431  zaddcllempos  9515  zaddcl  9518  zdiv  9567  deceq1  9614  deceq2  9615  uzaddcl  9819  zq  9859  qreccl  9875  cnref1o  9884  xaddnemnf  10091  xaddnepnf  10092  xaddcom  10095  xnn0xadd0  10101  xnegdi  10102  xaddass  10103  xlt2add  10114  xlesubadd  10117  xleaddadd  10121  fzsuc2  10313  fzrevral  10339  fzshftral  10342  2ffzeq  10375  exfzdc  10485  exbtwnzlemshrink  10507  rebtwn2zlemshrink  10512  modqval  10585  modqmuladd  10627  modqmuladdnn0  10629  frecuzrdgrrn  10669  frec2uzrdg  10670  frecuzrdgrcl  10671  frecuzrdgsuc  10675  frecuzrdgrclt  10676  frecuzrdgg  10677  frecuzrdgsuctlem  10684  frecfzennn  10687  uzsinds  10705  iseqvalcbv  10720  seq3val  10721  seqvalcd  10722  seqovcd  10728  seq3caopr3  10752  seq3caopr2  10754  seqcaopr2g  10755  seq3f1olemp  10776  seqf1og  10782  seq3id  10786  seq3homo  10788  seq3z  10789  seqhomog  10791  seqfeq4g  10792  seq3distr  10793  expp1  10807  expnegap0  10808  expcllem  10811  expcl2lemap  10812  m1expcl2  10822  expap0  10830  mulexp  10839  expadd  10842  expmul  10845  leexp2r  10854  leexp1a  10855  bernneq  10921  expnbnd  10924  modqexp  10927  nn0ltexp2  10970  expcan  10977  apexp1  10979  facdiv  10999  faclbnd3  11004  faclbnd6  11005  bcval  11010  bcpasc  11027  bccl  11028  fz1eqb  11051  omgadd  11064  hashunlem  11066  hashfzo  11085  hashfzp1  11087  iswrdinn0  11117  wrdnval  11143  eqwrd  11153  eqs1  11204  pfxeq  11276  ccatopth  11296  wrd2ind  11303  swrdccatin1  11305  swrdccatin2  11309  pfxccatin12lem2  11311  swrdccat3blem  11319  pfxccatid  11321  swrdccatin1d  11323  swrdccatin2d  11324  s2dmg  11370  shftfvalg  11378  shftfval  11381  cjth  11406  remim  11420  reim0b  11422  cjexp  11453  cnrecnv  11470  cvg1nlemcau  11544  cvg1nlemres  11545  recvguniq  11555  resqrexlemp1rp  11566  resqrexlemfp1  11569  resqrexlemlo  11573  resqrexlemgt0  11580  resqrexlemoverl  11581  resqrexlemglsq  11582  resqrexlemsqa  11584  resqrexlemex  11585  resqrex  11586  absexp  11639  recan  11669  climcn2  11869  subcn2  11871  summodc  11943  fsum3  11947  fsum3cvg3  11956  fsumrev  12003  fisum0diag2  12007  telfsumo  12026  fsumrelem  12031  binomlem  12043  binom  12044  binom1dif  12047  bcxmaslem1  12048  bcxmas  12049  isumshft  12050  divcnv  12057  arisum  12058  trireciplem  12060  expcnvap0  12062  expcnvre  12063  expcnv  12064  explecnv  12065  geosergap  12066  geolim  12071  geolim2  12072  geo2sum  12074  geo2lim  12076  geoisum  12077  geoisumr  12078  geoisum1  12079  geoisum1c  12080  cvgratnnlemsumlt  12088  cvgratz  12092  prodmodc  12138  fprodseq  12143  fprodcl2lem  12165  fprodfac  12175  fprodabs  12176  fprodrev  12179  eftvalcn  12217  efcvgfsum  12227  ege2le3  12231  efcj  12233  efaddlem  12234  efexp  12242  eftlub  12250  efgt1p2  12255  eflegeo  12261  sinval  12262  cosval  12263  demoivreALT  12334  divides  12349  dvdscmul  12378  dvds2ln  12384  dvdstr  12388  odd2np1lem  12432  odd2np1  12433  2tp1odd  12444  opeo  12457  omeo  12458  m1expe  12459  m1expo  12460  m1exp1  12461  divalglemnn  12478  divalglemeunn  12481  divalglemeuneg  12483  divalgmod  12487  ndvdssub  12490  bitsval  12503  bitsfzolem  12514  bitsinv1lem  12521  bitsinv1  12522  gcd0id  12549  bezoutlemnewy  12566  bezoutlema  12569  bezoutlemb  12570  bezoutlemex  12571  bezoutlemaz  12573  bezoutlembz  12574  gcdmultiple  12590  gcdmultiplez  12591  dvdsmulgcd  12595  rplpwr  12597  nn0seqcvgd  12612  dvdslcm  12640  lcmeq0  12642  lcmcl  12643  lcmneg  12645  lcmgcdlem  12648  lcmdvds  12650  lcmid  12651  lcmgcdeq  12654  coprmdvds  12663  mulgcddvds  12665  qredeq  12667  cncongr1  12674  cncongr2  12675  cncongrcoprm  12677  prmind2  12691  isprm6  12718  prmdvdsexp  12719  prmdvdsexpr  12721  sqrt2irr  12733  pw2dvdslemn  12736  pw2dvdseu  12739  oddpwdclemxy  12740  sqpweven  12746  2sqpwodd  12747  sqne2sq  12748  nn0gcdsq  12771  qden1elz  12776  phival  12784  dfphi2  12791  eulerthlemrprm  12800  eulerthlema  12801  prmdiv  12806  prmdiveq  12807  phisum  12812  odzval  12813  odzcllem  12814  odzdvds  12817  reumodprminv  12825  pythagtriplem3  12839  pythagtriplem18  12853  pythagtriplem19  12854  pclem0  12858  pclemub  12859  pclemdc  12860  pcprecl  12861  pcprendvds  12862  pcpremul  12865  pceulem  12866  pceu  12867  pczpre  12869  pcdiv  12874  pcqmul  12875  pcqcl  12878  pcexp  12881  pcxnn0cl  12882  pcxcl  12883  pcge0  12885  pcdvdsb  12892  pcneg  12897  pcabs  12898  pcgcd1  12900  pc2dvds  12902  pc11  12903  pcz  12904  pcprmpw2  12905  pcprmpw  12906  dvdsprmpweq  12907  dvdsprmpweqnn  12908  dvdsprmpweqle  12909  pcaddlem  12911  pcadd  12912  pcfac  12922  oddprmdvds  12926  prmpwdvds  12927  pockthi  12930  infpnlem2  12932  1arithlem1  12935  4sqlemffi  12968  4sqlem12  12974  2expltfac  13011  ennnfonelemnn0  13042  ennnfonelemr  13043  f1ovscpbl  13394  imasaddvallemg  13397  ercpbl  13413  mgm1  13452  mgmidmo  13454  mgmlrid  13461  lidrideqd  13463  lidrididd  13464  grpinvalem  13467  grpinva  13468  gsumfzval  13473  gsumval2  13479  isnsgrp  13488  sgrpass  13490  sgrp1  13493  mndinvmod  13527  imasmnd2  13534  mnd1  13537  mnd1id  13538  mhmpropd  13548  mhmlin  13549  insubm  13567  mhmima  13573  gsumwsubmcl  13578  gsumwmhm  13580  grpinvex  13592  grppropd  13599  dfgrp2  13609  grpidd2  13623  grpinvval  13625  grpinvid1  13634  grplrinv  13639  grpidinv2  13640  grpidinv  13641  grplcan  13644  grpidssd  13658  grpinvssd  13659  dfgrp3mlem  13680  dfgrp3m  13681  grplactcnv  13684  grp1  13688  imasgrp2  13696  mhmlem  13700  mulgnn0gsum  13714  mulginvcom  13733  mulgnn0ass  13744  mulgmodid  13747  issubg  13759  issubg2m  13775  issubg4m  13779  isnsg2  13789  nsgbi  13790  isnsg3  13793  elnmz  13794  nmzbi  13795  ghmlin  13834  ghmrn  13843  ghmnsgima  13854  conjghm  13862  conjnmz  13865  gsumfzconst  13927  rngdi  13952  rngdir  13953  srglz  13997  srgisid  13998  srglmhm  14005  ringid  14038  ringinvnz1ne0  14061  ringinvnzdiv  14062  ring1  14071  ringlghm  14073  imasring  14076  dvdsrtr  14114  lringuplu  14209  issubrng  14212  issubrng2  14223  issubrg  14234  issubrg2  14254  rrgeq0i  14277  rrgeq0  14278  unitrrg  14280  domneq0  14285  lmodlema  14305  islmodd  14306  rmodislmodlem  14363  rmodislmod  14364  lssclg  14377  lss1d  14396  rnglidlmcl  14493  quscrng  14546  cnfldexp  14590  gsumfzfsumlemm  14600  cnfldui  14602  expghmap  14620  zrhval  14630  zrhvalg  14631  znunit  14672  txdis1cn  15001  cnmptcom  15021  psmettri2  15051  isxmet2d  15071  xmeteq0  15082  xmettri2  15084  elblps  15113  elbl  15114  blssps  15150  blss  15151  ssblex  15154  blin2  15155  metss2  15221  comet  15222  bdmopn  15227  txmetcnp  15241  blssioo  15276  divcnap  15288  mpomulcn  15289  expcn  15292  cncfval  15295  cncfi  15301  mulc1cncf  15312  cdivcncfap  15327  mulcncf  15331  expcncf  15332  cnopnap  15334  ellimc3apf  15383  cnlimci  15396  limccnpcntop  15398  limccnp2lem  15399  reldvg  15402  eldvap  15405  dvexp  15434  dvexp2  15435  dvrecap  15436  elplyr  15463  elplyd  15464  ply1termlem  15465  plymullem1  15471  plyadd  15474  plymul  15475  plycoeid3  15480  plycolemc  15481  plyco  15482  plycj  15484  dvply1  15488  dvply2g  15489  sin0pilem2  15505  rpcxpmul2  15636  relogbcxpbap  15688  logbgcd1irr  15690  2irrexpq  15699  2irrexpqap  15701  dvdsppwf1o  15712  mpodvdsmulf1o  15713  fsumdvdsmul  15714  sgmppw  15715  1sgmprm  15717  perfect  15724  lgsneg  15752  lgsdilem  15755  lgsdir  15763  lgsdilem2  15764  lgsdi  15765  lgsne0  15766  lgsdirnn0  15775  lgsdinn0  15776  gausslemma2dlem4  15792  lgseisenlem2  15799  lgseisenlem3  15800  lgseisenlem4  15801  lgsquadlem1  15805  lgsquadlem2  15806  lgsquad2lem2  15810  2lgs  15832  2sqlem6  15848  2sqlem8  15851  2sqlem9  15852  2sqlem10  15853  wlkeq  16204  wlkl1loop  16208  uspgr2wlkeq  16215  upgr2wlkdc  16227  clwwlknonmpo  16278  trilpolemclim  16640  trilpolemcl  16641  trilpolemisumle  16642  trilpolemeq1  16644  trilpolemlt1  16645  trilpo  16647  trirec0  16648  redcwlpo  16659  nconstwlpolemgt0  16668  nconstwlpo  16670  neapmkv  16672