Theorem oveq2 5775

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

Syntax hints:   → wi 4   = wceq 1331  ⟨cop 3525  ‘cfv 5118  (class class class)co 5767

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-rex 2420  df-v 2683  df-un 3070  df-sn 3528  df-pr 3529  df-op 3531  df-uni 3732  df-br 3925  df-iota 5083  df-fv 5126  df-ov 5770

This theorem is referenced by:  oveq12  5776  oveq2i  5778  oveq2d  5783  ovanraleqv  5791  rspceov  5806  fovcl  5869  ovmpos  5887  ov2gf  5888  ovi3  5900  caovclg  5916  caovcomg  5919  caovassg  5922  caovcang  5925  caovcan  5928  caovordig  5929  caovordg  5931  caovord  5935  caovdig  5938  caovdirg  5941  caovimo  5957  grprinvlem  5958  grprinvd  5959  suppssov1  5972  off  5987  omv  6344  oeiv  6345  oasuc  6353  oawordriexmid  6359  omsuc  6361  nna0r  6367  nnm0r  6368  nnacl  6369  nnmcl  6370  nnacom  6373  nnaass  6374  nndi  6375  nnmass  6376  nnmsucr  6377  nnmcom  6378  nnaordi  6397  nnaord  6398  nnmordi  6405  nnmord  6406  nnaordex  6416  nnawordex  6417  nnm00  6418  eroveu  6513  ecopovtrn  6519  ecopovtrng  6522  th3qlem2  6525  th3q  6527  ecovcom  6529  ecovicom  6530  ecovass  6531  ecoviass  6532  ecovdi  6533  ecovidi  6534  addcanpig  7135  mulcanpig  7136  addcmpblnq  7168  addclnq  7176  mulclnq  7177  recexnq  7191  recmulnqg  7192  ltanqg  7201  ltmnqg  7202  ltexnqq  7209  enq0ref  7234  enq0tr  7235  addcmpblnq0  7244  mulnnnq0  7251  addclnq0  7252  mulclnq0  7253  distrnq0  7260  mulcomnq0  7261  addassnq0  7263  nq02m  7266  prarloclem3  7298  genipv  7310  genpassl  7325  genpassu  7326  addlocpr  7337  distrlem1prl  7383  distrlem1pru  7384  1idprl  7391  1idpru  7392  ltexprlemell  7399  ltexprlemelu  7400  ltexpri  7414  lteupri  7418  ltaprlem  7419  recexprlem1ssl  7434  recexprlem1ssu  7435  recexpr  7439  cauappcvgprlemm  7446  cauappcvgprlemdisj  7452  cauappcvgprlemloc  7453  cauappcvgprlemladdru  7457  cauappcvgprlemladdrl  7458  cauappcvgprlem1  7460  cauappcvgprlemlim  7462  cauappcvgpr  7463  mulcmpblnrlemg  7541  addclsr  7554  mulclsr  7555  ltasrg  7571  negexsr  7573  recexgt0sr  7574  mulgt0sr  7579  mulextsr1  7582  srpospr  7584  caucvgsrlemgt1  7596  map2psrprg  7606  axaddrcl  7666  axmulrcl  7668  axaddcom  7671  axrnegex  7680  axprecex  7681  axcnre  7682  axpre-ltadd  7687  axpre-mulgt0  7688  axpre-mulext  7689  rereceu  7690  recriota  7691  axcaucvglemres  7700  readdcan  7895  cnegexlem1  7930  cnegex  7933  addcan  7935  negeq  7948  subadd  7958  addid0  8128  ine0  8149  rimul  8340  cru  8357  apreim  8358  recexap  8407  mulcanapd  8415  receuap  8423  divmulap  8428  cju  8712  nnaddcl  8733  nnmulcl  8734  nnsub  8752  nnnn0addcl  9000  zaddcllempos  9084  zaddcl  9087  zdiv  9132  deceq1  9179  deceq2  9180  uzaddcl  9374  zq  9411  qreccl  9427  cnref1o  9433  xaddnemnf  9633  xaddnepnf  9634  xaddcom  9637  xnn0xadd0  9643  xnegdi  9644  xaddass  9645  xlt2add  9656  xlesubadd  9659  xleaddadd  9663  fzsuc2  9852  fzrevral  9878  fzshftral  9881  2ffzeq  9911  exfzdc  10010  exbtwnzlemshrink  10019  rebtwn2zlemshrink  10024  modqval  10090  modqmuladd  10132  modqmuladdnn0  10134  frecuzrdgrrn  10174  frec2uzrdg  10175  frecuzrdgrcl  10176  frecuzrdgsuc  10180  frecuzrdgrclt  10181  frecuzrdgg  10182  frecuzrdgsuctlem  10189  frecfzennn  10192  uzsinds  10208  iseqvalcbv  10223  seq3val  10224  seqvalcd  10225  seqovcd  10229  seq3caopr3  10247  seq3caopr2  10248  seq3f1olemp  10268  seq3id  10274  seq3homo  10276  seq3z  10277  seq3distr  10279  expp1  10293  expnegap0  10294  expcllem  10297  expcl2lemap  10298  m1expcl2  10308  expap0  10316  mulexp  10325  expadd  10328  expmul  10331  leexp2r  10340  leexp1a  10341  bernneq  10405  expnbnd  10408  expcan  10456  facdiv  10477  faclbnd3  10482  faclbnd6  10483  bcval  10488  bcpasc  10505  bccl  10506  fz1eqb  10530  omgadd  10541  hashunlem  10543  hashfzo  10561  hashfzp1  10563  shftfvalg  10583  shftfval  10586  cjth  10611  remim  10625  reim0b  10627  cjexp  10658  cnrecnv  10675  cvg1nlemcau  10749  cvg1nlemres  10750  recvguniq  10760  resqrexlemp1rp  10771  resqrexlemfp1  10774  resqrexlemlo  10778  resqrexlemgt0  10785  resqrexlemoverl  10786  resqrexlemglsq  10787  resqrexlemsqa  10789  resqrexlemex  10790  resqrex  10791  absexp  10844  recan  10874  climcn2  11071  subcn2  11073  summodc  11145  fsum3  11149  fsum3cvg3  11158  fsumrev  11205  fisum0diag2  11209  telfsumo  11228  fsumrelem  11233  binomlem  11245  binom  11246  binom1dif  11249  bcxmaslem1  11250  bcxmas  11251  isumshft  11252  divcnv  11259  arisum  11260  trireciplem  11262  expcnvap0  11264  expcnvre  11265  expcnv  11266  explecnv  11267  geosergap  11268  geolim  11273  geolim2  11274  geo2sum  11276  geo2lim  11278  geoisum  11279  geoisumr  11280  geoisum1  11281  geoisum1c  11282  cvgratnnlemsumlt  11290  cvgratz  11294  eftvalcn  11352  efcvgfsum  11362  ege2le3  11366  efcj  11368  efaddlem  11369  efexp  11377  eftlub  11385  efgt1p2  11390  eflegeo  11397  sinval  11398  cosval  11399  demoivreALT  11469  divides  11484  dvdscmul  11509  dvds2ln  11515  dvdstr  11519  odd2np1lem  11558  odd2np1  11559  2tp1odd  11570  opeo  11583  omeo  11584  m1expe  11585  m1expo  11586  m1exp1  11587  divalglemnn  11604  divalglemeunn  11607  divalglemeuneg  11609  divalgmod  11613  ndvdssub  11616  gcd0id  11656  bezoutlemnewy  11673  bezoutlema  11676  bezoutlemb  11677  bezoutlemex  11678  bezoutlemaz  11680  bezoutlembz  11681  gcdmultiple  11697  gcdmultiplez  11698  dvdsmulgcd  11702  rplpwr  11704  nn0seqcvgd  11711  dvdslcm  11739  lcmeq0  11741  lcmcl  11742  lcmneg  11744  lcmgcdlem  11747  lcmdvds  11749  lcmid  11750  lcmgcdeq  11753  coprmdvds  11762  mulgcddvds  11764  qredeq  11766  cncongr1  11773  cncongr2  11774  cncongrcoprm  11776  prmind2  11790  isprm6  11814  prmdvdsexp  11815  prmdvdsexpr  11817  sqrt2irr  11829  pw2dvdslemn  11832  pw2dvdseu  11835  oddpwdclemxy  11836  sqpweven  11842  2sqpwodd  11843  sqne2sq  11844  nn0gcdsq  11867  qden1elz  11872  phival  11878  dfphi2  11885  ennnfonelemnn0  11924  ennnfonelemr  11925  txdis1cn  12436  cnmptcom  12456  psmettri2  12486  isxmet2d  12506  xmeteq0  12517  xmettri2  12519  elblps  12548  elbl  12549  blssps  12585  blss  12586  ssblex  12589  blin2  12590  metss2  12656  comet  12657  bdmopn  12662  txmetcnp  12676  blssioo  12703  divcnap  12713  cncfval  12717  cncfi  12723  mulc1cncf  12734  cdivcncfap  12745  mulcncf  12749  expcncf  12750  cnopnap  12752  ellimc3apf  12787  cnlimci  12800  limccnpcntop  12802  limccnp2lem  12803  reldvg  12806  eldvap  12809  dvexp  12833  dvexp2  12834  dvrecap  12835  sin0pilem2  12852  trilpolemclim  13218  trilpolemcl  13219  trilpolemisumle  13220  trilpolemeq1  13222  trilpolemlt1  13223  trilpo  13225