Theorem oveq2 5734

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

Syntax hints:   → wi 4   = wceq 1312  ⟨cop 3494  ‘cfv 5079  (class class class)co 5726

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-3an 945  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-rex 2394  df-v 2657  df-un 3039  df-sn 3497  df-pr 3498  df-op 3500  df-uni 3701  df-br 3894  df-iota 5044  df-fv 5087  df-ov 5729

This theorem is referenced by:  oveq12  5735  oveq2i  5737  oveq2d  5742  ovanraleqv  5750  rspceov  5765  fovcl  5828  ovmpos  5846  ov2gf  5847  ovi3  5859  caovclg  5875  caovcomg  5878  caovassg  5881  caovcang  5884  caovcan  5887  caovordig  5888  caovordg  5890  caovord  5894  caovdig  5897  caovdirg  5900  caovimo  5916  grprinvlem  5917  grprinvd  5918  suppssov1  5931  off  5946  omv  6303  oeiv  6304  oasuc  6312  oawordriexmid  6318  omsuc  6320  nna0r  6326  nnm0r  6327  nnacl  6328  nnmcl  6329  nnacom  6332  nnaass  6333  nndi  6334  nnmass  6335  nnmsucr  6336  nnmcom  6337  nnaordi  6356  nnaord  6357  nnmordi  6364  nnmord  6365  nnaordex  6375  nnawordex  6376  nnm00  6377  eroveu  6472  ecopovtrn  6478  ecopovtrng  6481  th3qlem2  6484  th3q  6486  ecovcom  6488  ecovicom  6489  ecovass  6490  ecoviass  6491  ecovdi  6492  ecovidi  6493  addcanpig  7084  mulcanpig  7085  addcmpblnq  7117  addclnq  7125  mulclnq  7126  recexnq  7140  recmulnqg  7141  ltanqg  7150  ltmnqg  7151  ltexnqq  7158  enq0ref  7183  enq0tr  7184  addcmpblnq0  7193  mulnnnq0  7200  addclnq0  7201  mulclnq0  7202  distrnq0  7209  mulcomnq0  7210  addassnq0  7212  nq02m  7215  prarloclem3  7247  genipv  7259  genpassl  7274  genpassu  7275  addlocpr  7286  distrlem1prl  7332  distrlem1pru  7333  1idprl  7340  1idpru  7341  ltexprlemell  7348  ltexprlemelu  7349  ltexpri  7363  lteupri  7367  ltaprlem  7368  recexprlem1ssl  7383  recexprlem1ssu  7384  recexpr  7388  cauappcvgprlemm  7395  cauappcvgprlemdisj  7401  cauappcvgprlemloc  7402  cauappcvgprlemladdru  7406  cauappcvgprlemladdrl  7407  cauappcvgprlem1  7409  cauappcvgprlemlim  7411  cauappcvgpr  7412  mulcmpblnrlemg  7477  addclsr  7490  mulclsr  7491  ltasrg  7507  negexsr  7509  recexgt0sr  7510  mulgt0sr  7514  mulextsr1  7517  srpospr  7519  caucvgsrlemgt1  7531  axaddrcl  7594  axmulrcl  7596  axaddcom  7599  axrnegex  7608  axprecex  7609  axcnre  7610  axpre-ltadd  7615  axpre-mulgt0  7616  axpre-mulext  7617  rereceu  7618  recriota  7619  axcaucvglemres  7628  readdcan  7819  cnegexlem1  7854  cnegex  7857  addcan  7859  negeq  7872  subadd  7882  addid0  8048  ine0  8069  rimul  8259  cru  8276  apreim  8277  recexap  8321  mulcanapd  8329  receuap  8337  divmulap  8342  cju  8623  nnaddcl  8644  nnmulcl  8645  nnsub  8663  nnnn0addcl  8905  zaddcllempos  8989  zaddcl  8992  zdiv  9037  deceq1  9084  deceq2  9085  uzaddcl  9277  zq  9314  qreccl  9330  cnref1o  9336  xaddnemnf  9527  xaddnepnf  9528  xaddcom  9531  xnn0xadd0  9537  xnegdi  9538  xaddass  9539  xlt2add  9550  xlesubadd  9553  xleaddadd  9557  fzsuc2  9746  fzrevral  9772  fzshftral  9775  2ffzeq  9805  exfzdc  9904  exbtwnzlemshrink  9913  rebtwn2zlemshrink  9918  modqval  9984  modqmuladd  10026  modqmuladdnn0  10028  frecuzrdgrrn  10068  frec2uzrdg  10069  frecuzrdgrcl  10070  frecuzrdgsuc  10074  frecuzrdgrclt  10075  frecuzrdgg  10076  frecuzrdgsuctlem  10083  frecfzennn  10086  uzsinds  10102  iseqvalcbv  10117  seq3val  10118  seqvalcd  10119  seqovcd  10123  seq3caopr3  10141  seq3caopr2  10142  seq3f1olemp  10162  seq3id  10168  seq3homo  10170  seq3z  10171  seq3distr  10173  expp1  10187  expnegap0  10188  expcllem  10191  expcl2lemap  10192  m1expcl2  10202  expap0  10210  mulexp  10219  expadd  10222  expmul  10225  leexp2r  10234  leexp1a  10235  bernneq  10299  expnbnd  10302  expcan  10350  facdiv  10371  faclbnd3  10376  faclbnd6  10377  bcval  10382  bcpasc  10399  bccl  10400  fz1eqb  10424  omgadd  10435  hashunlem  10437  hashfzo  10455  hashfzp1  10457  shftfvalg  10477  shftfval  10480  cjth  10505  remim  10519  reim0b  10521  cjexp  10552  cnrecnv  10569  cvg1nlemcau  10642  cvg1nlemres  10643  recvguniq  10653  resqrexlemp1rp  10664  resqrexlemfp1  10667  resqrexlemlo  10671  resqrexlemgt0  10678  resqrexlemoverl  10679  resqrexlemglsq  10680  resqrexlemsqa  10682  resqrexlemex  10683  resqrex  10684  absexp  10737  recan  10767  climcn2  10964  subcn2  10966  summodc  11038  fsum3  11042  fsum3cvg3  11051  fsumrev  11098  fisum0diag2  11102  telfsumo  11121  fsumrelem  11126  binomlem  11138  binom  11139  binom1dif  11142  bcxmaslem1  11143  bcxmas  11144  isumshft  11145  divcnv  11152  arisum  11153  trireciplem  11155  expcnvap0  11157  expcnvre  11158  expcnv  11159  explecnv  11160  geosergap  11161  geolim  11166  geolim2  11167  geo2sum  11169  geo2lim  11171  geoisum  11172  geoisumr  11173  geoisum1  11174  geoisum1c  11175  cvgratnnlemsumlt  11183  cvgratz  11187  eftvalcn  11208  efcvgfsum  11218  ege2le3  11222  efcj  11224  efaddlem  11225  efexp  11233  eftlub  11241  efgt1p2  11246  eflegeo  11253  sinval  11254  cosval  11255  demoivreALT  11324  divides  11337  dvdscmul  11362  dvds2ln  11368  dvdstr  11372  odd2np1lem  11411  odd2np1  11412  2tp1odd  11423  opeo  11436  omeo  11437  m1expe  11438  m1expo  11439  m1exp1  11440  divalglemnn  11457  divalglemeunn  11460  divalglemeuneg  11462  divalgmod  11466  ndvdssub  11469  gcd0id  11509  bezoutlemnewy  11524  bezoutlema  11527  bezoutlemb  11528  bezoutlemex  11529  bezoutlemaz  11531  bezoutlembz  11532  gcdmultiple  11548  gcdmultiplez  11549  dvdsmulgcd  11553  rplpwr  11555  nn0seqcvgd  11562  dvdslcm  11590  lcmeq0  11592  lcmcl  11593  lcmneg  11595  lcmgcdlem  11598  lcmdvds  11600  lcmid  11601  lcmgcdeq  11604  coprmdvds  11613  mulgcddvds  11615  qredeq  11617  cncongr1  11624  cncongr2  11625  cncongrcoprm  11627  prmind2  11641  isprm6  11665  prmdvdsexp  11666  prmdvdsexpr  11668  sqrt2irr  11680  pw2dvdslemn  11682  pw2dvdseu  11685  oddpwdclemxy  11686  sqpweven  11692  2sqpwodd  11693  sqne2sq  11694  nn0gcdsq  11717  qden1elz  11722  phival  11728  dfphi2  11735  ennnfonelemnn0  11774  ennnfonelemr  11775  txdis1cn  12283  cnmptcom  12303  psmettri2  12311  isxmet2d  12331  xmeteq0  12342  xmettri2  12344  elblps  12373  elbl  12374  blssps  12410  blss  12411  ssblex  12414  blin2  12415  metss2  12481  comet  12482  bdmopn  12487  txmetcnp  12501  blssioo  12525  divcnap  12535  cncfval  12539  cncfi  12545  mulc1cncf  12556  cdivcncfap  12567  mulcncf  12571  expcncf  12572  ellimc3apf  12579  cnlimci  12592  limccnpcntop  12594  limccnp2lem  12595  reldvg  12597  eldvap  12600  trilpolemclim  12910  trilpolemcl  12911  trilpolemisumle  12912  trilpolemeq1  12914  trilpolemlt1  12915  trilpo  12917