Theorem oveq2 6026

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

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

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 6021

This theorem is referenced by:  oveq12  6027  oveq2i  6029  oveq2d  6034  ovanraleqv  6042  ovrspc2v  6044  oveqrspc2v  6045  rspceov  6061  fovcld  6126  ovmpos  6145  ov2gf  6146  ovi3  6159  caovclg  6175  caovcomg  6178  caovassg  6181  caovcang  6184  caovcan  6187  caovordig  6188  caovordg  6190  caovord  6194  caovdig  6197  caovdirg  6200  caovimo  6216  suppssov1  6232  off  6248  caofid0l  6262  caofid2  6265  caofdig  6269  omv  6623  oeiv  6624  oasuc  6632  oawordriexmid  6638  omsuc  6640  nna0r  6646  nnm0r  6647  nnacl  6648  nnmcl  6649  nnacom  6652  nnaass  6653  nndi  6654  nnmass  6655  nnmsucr  6656  nnmcom  6657  nnaordi  6676  nnaord  6677  nnmordi  6684  nnmord  6685  nnaordex  6696  nnawordex  6697  nnm00  6698  eroveu  6795  ecopovtrn  6801  ecopovtrng  6804  th3qlem2  6807  th3q  6809  ecovcom  6811  ecovicom  6812  ecovass  6813  ecoviass  6814  ecovdi  6815  ecovidi  6816  exmidpw2en  7104  acneq  7417  addcanpig  7554  mulcanpig  7555  addcmpblnq  7587  addclnq  7595  mulclnq  7596  recexnq  7610  recmulnqg  7611  ltanqg  7620  ltmnqg  7621  ltexnqq  7628  enq0ref  7653  enq0tr  7654  addcmpblnq0  7663  mulnnnq0  7670  addclnq0  7671  mulclnq0  7672  distrnq0  7679  mulcomnq0  7680  addassnq0  7682  nq02m  7685  prarloclem3  7717  genipv  7729  genpassl  7744  genpassu  7745  addlocpr  7756  distrlem1prl  7802  distrlem1pru  7803  1idprl  7810  1idpru  7811  ltexprlemell  7818  ltexprlemelu  7819  ltexpri  7833  lteupri  7837  ltaprlem  7838  recexprlem1ssl  7853  recexprlem1ssu  7854  recexpr  7858  cauappcvgprlemm  7865  cauappcvgprlemdisj  7871  cauappcvgprlemloc  7872  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  cauappcvgprlem1  7879  cauappcvgprlemlim  7881  cauappcvgpr  7882  mulcmpblnrlemg  7960  addclsr  7973  mulclsr  7974  ltasrg  7990  negexsr  7992  recexgt0sr  7993  mulgt0sr  7998  mulextsr1  8001  srpospr  8003  caucvgsrlemgt1  8015  map2psrprg  8025  axaddrcl  8085  axmulrcl  8087  axaddcom  8090  axrnegex  8099  axprecex  8100  axcnre  8101  axpre-ltadd  8106  axpre-mulgt0  8107  axpre-mulext  8108  rereceu  8109  recriota  8110  axcaucvglemres  8119  readdcan  8319  cnegexlem1  8354  cnegex  8357  addcan  8359  negeq  8372  subadd  8382  addid0  8552  ine0  8573  rimul  8765  cru  8782  apreim  8783  recexap  8833  mulcanapd  8841  receuap  8849  divmulap  8855  rerecapb  9023  cju  9141  nnaddcl  9163  nnmulcl  9164  nnsub  9182  nnnn0addcl  9432  zaddcllempos  9516  zaddcl  9519  zdiv  9568  deceq1  9615  deceq2  9616  uzaddcl  9820  zq  9860  qreccl  9876  cnref1o  9885  xaddnemnf  10092  xaddnepnf  10093  xaddcom  10096  xnn0xadd0  10102  xnegdi  10103  xaddass  10104  xlt2add  10115  xlesubadd  10118  xleaddadd  10122  fzsuc2  10314  fzrevral  10340  fzshftral  10343  2ffzeq  10376  exfzdc  10487  exbtwnzlemshrink  10509  rebtwn2zlemshrink  10514  modqval  10587  modqmuladd  10629  modqmuladdnn0  10631  frecuzrdgrrn  10671  frec2uzrdg  10672  frecuzrdgrcl  10673  frecuzrdgsuc  10677  frecuzrdgrclt  10678  frecuzrdgg  10679  frecuzrdgsuctlem  10686  frecfzennn  10689  uzsinds  10707  iseqvalcbv  10722  seq3val  10723  seqvalcd  10724  seqovcd  10730  seq3caopr3  10754  seq3caopr2  10756  seqcaopr2g  10757  seq3f1olemp  10778  seqf1og  10784  seq3id  10788  seq3homo  10790  seq3z  10791  seqhomog  10793  seqfeq4g  10794  seq3distr  10795  expp1  10809  expnegap0  10810  expcllem  10813  expcl2lemap  10814  m1expcl2  10824  expap0  10832  mulexp  10841  expadd  10844  expmul  10847  leexp2r  10856  leexp1a  10857  bernneq  10923  expnbnd  10926  modqexp  10929  nn0ltexp2  10972  expcan  10979  apexp1  10981  facdiv  11001  faclbnd3  11006  faclbnd6  11007  bcval  11012  bcpasc  11029  bccl  11030  fz1eqb  11053  omgadd  11066  hashunlem  11068  hashfzo  11087  hashfzp1  11089  iswrdinn0  11122  wrdnval  11148  eqwrd  11158  eqs1  11209  pfxeq  11281  ccatopth  11301  wrd2ind  11308  swrdccatin1  11310  swrdccatin2  11314  pfxccatin12lem2  11316  swrdccat3blem  11324  pfxccatid  11326  swrdccatin1d  11328  swrdccatin2d  11329  s2dmg  11375  shftfvalg  11396  shftfval  11399  cjth  11424  remim  11438  reim0b  11440  cjexp  11471  cnrecnv  11488  cvg1nlemcau  11562  cvg1nlemres  11563  recvguniq  11573  resqrexlemp1rp  11584  resqrexlemfp1  11587  resqrexlemlo  11591  resqrexlemgt0  11598  resqrexlemoverl  11599  resqrexlemglsq  11600  resqrexlemsqa  11602  resqrexlemex  11603  resqrex  11604  absexp  11657  recan  11687  climcn2  11887  subcn2  11889  summodc  11962  fsum3  11966  fsum3cvg3  11975  fsumrev  12022  fisum0diag2  12026  telfsumo  12045  fsumrelem  12050  binomlem  12062  binom  12063  binom1dif  12066  bcxmaslem1  12067  bcxmas  12068  isumshft  12069  divcnv  12076  arisum  12077  trireciplem  12079  expcnvap0  12081  expcnvre  12082  expcnv  12083  explecnv  12084  geosergap  12085  geolim  12090  geolim2  12091  geo2sum  12093  geo2lim  12095  geoisum  12096  geoisumr  12097  geoisum1  12098  geoisum1c  12099  cvgratnnlemsumlt  12107  cvgratz  12111  prodmodc  12157  fprodseq  12162  fprodcl2lem  12184  fprodfac  12194  fprodabs  12195  fprodrev  12198  eftvalcn  12236  efcvgfsum  12246  ege2le3  12250  efcj  12252  efaddlem  12253  efexp  12261  eftlub  12269  efgt1p2  12274  eflegeo  12280  sinval  12281  cosval  12282  demoivreALT  12353  divides  12368  dvdscmul  12397  dvds2ln  12403  dvdstr  12407  odd2np1lem  12451  odd2np1  12452  2tp1odd  12463  opeo  12476  omeo  12477  m1expe  12478  m1expo  12479  m1exp1  12480  divalglemnn  12497  divalglemeunn  12500  divalglemeuneg  12502  divalgmod  12506  ndvdssub  12509  bitsval  12522  bitsfzolem  12533  bitsinv1lem  12540  bitsinv1  12541  gcd0id  12568  bezoutlemnewy  12585  bezoutlema  12588  bezoutlemb  12589  bezoutlemex  12590  bezoutlemaz  12592  bezoutlembz  12593  gcdmultiple  12609  gcdmultiplez  12610  dvdsmulgcd  12614  rplpwr  12616  nn0seqcvgd  12631  dvdslcm  12659  lcmeq0  12661  lcmcl  12662  lcmneg  12664  lcmgcdlem  12667  lcmdvds  12669  lcmid  12670  lcmgcdeq  12673  coprmdvds  12682  mulgcddvds  12684  qredeq  12686  cncongr1  12693  cncongr2  12694  cncongrcoprm  12696  prmind2  12710  isprm6  12737  prmdvdsexp  12738  prmdvdsexpr  12740  sqrt2irr  12752  pw2dvdslemn  12755  pw2dvdseu  12758  oddpwdclemxy  12759  sqpweven  12765  2sqpwodd  12766  sqne2sq  12767  nn0gcdsq  12790  qden1elz  12795  phival  12803  dfphi2  12810  eulerthlemrprm  12819  eulerthlema  12820  prmdiv  12825  prmdiveq  12826  phisum  12831  odzval  12832  odzcllem  12833  odzdvds  12836  reumodprminv  12844  pythagtriplem3  12858  pythagtriplem18  12872  pythagtriplem19  12873  pclem0  12877  pclemub  12878  pclemdc  12879  pcprecl  12880  pcprendvds  12881  pcpremul  12884  pceulem  12885  pceu  12886  pczpre  12888  pcdiv  12893  pcqmul  12894  pcqcl  12897  pcexp  12900  pcxnn0cl  12901  pcxcl  12902  pcge0  12904  pcdvdsb  12911  pcneg  12916  pcabs  12917  pcgcd1  12919  pc2dvds  12921  pc11  12922  pcz  12923  pcprmpw2  12924  pcprmpw  12925  dvdsprmpweq  12926  dvdsprmpweqnn  12927  dvdsprmpweqle  12928  pcaddlem  12930  pcadd  12931  pcfac  12941  oddprmdvds  12945  prmpwdvds  12946  pockthi  12949  infpnlem2  12951  1arithlem1  12954  4sqlemffi  12987  4sqlem12  12993  2expltfac  13030  ennnfonelemnn0  13061  ennnfonelemr  13062  f1ovscpbl  13413  imasaddvallemg  13416  ercpbl  13432  mgm1  13471  mgmidmo  13473  mgmlrid  13480  lidrideqd  13482  lidrididd  13483  grpinvalem  13486  grpinva  13487  gsumfzval  13492  gsumval2  13498  isnsgrp  13507  sgrpass  13509  sgrp1  13512  mndinvmod  13546  imasmnd2  13553  mnd1  13556  mnd1id  13557  mhmpropd  13567  mhmlin  13568  insubm  13586  mhmima  13592  gsumwsubmcl  13597  gsumwmhm  13599  grpinvex  13611  grppropd  13618  dfgrp2  13628  grpidd2  13642  grpinvval  13644  grpinvid1  13653  grplrinv  13658  grpidinv2  13659  grpidinv  13660  grplcan  13663  grpidssd  13677  grpinvssd  13678  dfgrp3mlem  13699  dfgrp3m  13700  grplactcnv  13703  grp1  13707  imasgrp2  13715  mhmlem  13719  mulgnn0gsum  13733  mulginvcom  13752  mulgnn0ass  13763  mulgmodid  13766  issubg  13778  issubg2m  13794  issubg4m  13798  isnsg2  13808  nsgbi  13809  isnsg3  13812  elnmz  13813  nmzbi  13814  ghmlin  13853  ghmrn  13862  ghmnsgima  13873  conjghm  13881  conjnmz  13884  gsumfzconst  13946  rngdi  13972  rngdir  13973  srglz  14017  srgisid  14018  srglmhm  14025  ringid  14058  ringinvnz1ne0  14081  ringinvnzdiv  14082  ring1  14091  ringlghm  14093  imasring  14096  dvdsrtr  14134  lringuplu  14229  issubrng  14232  issubrng2  14243  issubrg  14254  issubrg2  14274  rrgeq0i  14297  rrgeq0  14298  unitrrg  14300  domneq0  14305  lmodlema  14325  islmodd  14326  rmodislmodlem  14383  rmodislmod  14384  lssclg  14397  lss1d  14416  rnglidlmcl  14513  quscrng  14566  cnfldexp  14610  gsumfzfsumlemm  14620  cnfldui  14622  expghmap  14640  zrhval  14650  zrhvalg  14651  znunit  14692  txdis1cn  15021  cnmptcom  15041  psmettri2  15071  isxmet2d  15091  xmeteq0  15102  xmettri2  15104  elblps  15133  elbl  15134  blssps  15170  blss  15171  ssblex  15174  blin2  15175  metss2  15241  comet  15242  bdmopn  15247  txmetcnp  15261  blssioo  15296  divcnap  15308  mpomulcn  15309  expcn  15312  cncfval  15315  cncfi  15321  mulc1cncf  15332  cdivcncfap  15347  mulcncf  15351  expcncf  15352  cnopnap  15354  ellimc3apf  15403  cnlimci  15416  limccnpcntop  15418  limccnp2lem  15419  reldvg  15422  eldvap  15425  dvexp  15454  dvexp2  15455  dvrecap  15456  elplyr  15483  elplyd  15484  ply1termlem  15485  plymullem1  15491  plyadd  15494  plymul  15495  plycoeid3  15500  plycolemc  15501  plyco  15502  plycj  15504  dvply1  15508  dvply2g  15509  sin0pilem2  15525  rpcxpmul2  15656  relogbcxpbap  15708  logbgcd1irr  15710  2irrexpq  15719  2irrexpqap  15721  dvdsppwf1o  15732  mpodvdsmulf1o  15733  fsumdvdsmul  15734  sgmppw  15735  1sgmprm  15737  perfect  15744  lgsneg  15772  lgsdilem  15775  lgsdir  15783  lgsdilem2  15784  lgsdi  15785  lgsne0  15786  lgsdirnn0  15795  lgsdinn0  15796  gausslemma2dlem4  15812  lgseisenlem2  15819  lgseisenlem3  15820  lgseisenlem4  15821  lgsquadlem1  15825  lgsquadlem2  15826  lgsquad2lem2  15830  2lgs  15852  2sqlem6  15868  2sqlem8  15871  2sqlem9  15872  2sqlem10  15873  wlkeq  16224  wlkl1loop  16228  uspgr2wlkeq  16235  upgr2wlkdc  16247  clwwlknonmpo  16298  eupth2fi  16349  trilpolemclim  16691  trilpolemcl  16692  trilpolemisumle  16693  trilpolemeq1  16695  trilpolemlt1  16696  trilpo  16698  trirec0  16699  qdiff  16704  redcwlpo  16711  nconstwlpolemgt0  16720  nconstwlpo  16722  neapmkv  16724