Theorem oveq2 5463

Description: Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)

Assertion

Ref	Expression
oveq2	⊢ (A = B → (𝐶𝐹A) = (𝐶𝐹B))

Proof of Theorem oveq2

Step	Hyp	Ref	Expression
1		opeq2 3541	. . 3 ⊢ (A = B → ⟨𝐶, A⟩ = ⟨𝐶, B⟩)
2	1	fveq2d 5125	. 2 ⊢ (A = B → (𝐹‘⟨𝐶, A⟩) = (𝐹‘⟨𝐶, B⟩))
3		df-ov 5458	. 2 ⊢ (𝐶𝐹A) = (𝐹‘⟨𝐶, A⟩)
4		df-ov 5458	. 2 ⊢ (𝐶𝐹B) = (𝐹‘⟨𝐶, B⟩)
5	2, 3, 4	3eqtr4g 2094	1 ⊢ (A = B → (𝐶𝐹A) = (𝐶𝐹B))

Syntax hints:   → wi 4   = wceq 1242  ⟨cop 3370  ‘cfv 4845  (class class class)co 5455

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-rex 2306  df-v 2553  df-un 2916  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-iota 4810  df-fv 4853  df-ov 5458

This theorem is referenced by:  oveq12  5464  oveq2i  5466  oveq2d  5471  rspceov  5489  fovcl  5548  ovmpt2s  5566  ov2gf  5567  ovi3  5579  caovclg  5595  caovcomg  5598  caovassg  5601  caovcang  5604  caovcan  5607  caovordig  5608  caovordg  5610  caovord  5614  caovdig  5617  caovdirg  5620  caovimo  5636  grprinvlem  5637  grprinvd  5638  suppssov1  5651  off  5666  omv  5974  oeiv  5975  oasuc  5983  omsuc  5990  nna0r  5996  nnm0r  5997  nnacl  5998  nnmcl  5999  nnacom  6002  nnaass  6003  nndi  6004  nnmass  6005  nnmsucr  6006  nnmcom  6007  nnaordi  6017  nnaord  6018  nnmordi  6025  nnmord  6026  nnaordex  6036  nnawordex  6037  nnm00  6038  eroveu  6133  ecopovtrn  6139  ecopovtrng  6142  th3qlem2  6145  th3q  6147  ecovcom  6149  ecovicom  6150  ecovass  6151  ecoviass  6152  ecovdi  6153  ecovidi  6154  addcanpig  6318  mulcanpig  6319  addcmpblnq  6351  addclnq  6359  mulclnq  6360  recexnq  6374  recmulnqg  6375  ltanqg  6384  ltmnqg  6385  ltexnqq  6391  enq0ref  6416  enq0tr  6417  addcmpblnq0  6426  mulnnnq0  6433  addclnq0  6434  mulclnq0  6435  distrnq0  6442  mulcomnq0  6443  addassnq0  6445  nq02m  6448  prarloclem3  6480  genipv  6492  genpassl  6507  genpassu  6508  addlocpr  6519  distrlem1prl  6558  distrlem1pru  6559  1idprl  6566  1idpru  6567  ltexprlemell  6572  ltexprlemelu  6573  ltexpri  6587  ltaprlem  6591  recexprlem1ssl  6605  recexprlem1ssu  6606  recexpr  6610  cauappcvgprlemm  6617  cauappcvgprlemdisj  6623  cauappcvgprlemloc  6624  cauappcvgprlemladdru  6628  cauappcvgprlemladdrl  6629  cauappcvgprlem1  6631  cauappcvgprlemlim  6633  cauappcvgpr  6634  mulcmpblnrlemg  6668  addclsr  6681  mulclsr  6682  ltasrg  6698  negexsr  6700  recexgt0sr  6701  mulgt0sr  6704  mulextsr1  6707  axaddrcl  6751  axmulrcl  6753  axaddcom  6754  axrnegex  6763  axprecex  6764  axcnre  6765  axpre-ltadd  6770  axpre-mulgt0  6771  axpre-mulext  6772  readdcan  6950  cnegexlem1  6983  cnegex  6986  addcan  6988  negeq  7001  subadd  7011  ine0  7187  rimul  7369  cru  7386  apreim  7387  recexap  7416  mulcanapd  7424  receuap  7432  divmulap  7436  cju  7694  nnaddcl  7715  nnmulcl  7716  nnsub  7733  nnnn0addcl  7988  zaddcllempos  8058  zaddcl  8061  zdiv  8104  deceq1  8146  deceq2  8147  uzaddcl  8305  zq  8337  qreccl  8351  cnref1o  8357  fzsuc2  8711  fzrevral  8737  fzshftral  8740  2ffzeq  8768  frecuzrdgrrn  8875  frec2uzrdg  8876  frecuzrdgsuc  8882  frecfzennn  8884  expp1  8916  expnegap0  8917  expcllem  8920  expcl2lemap  8921  m1expcl2  8931  expap0  8939  mulexp  8948  expadd  8951  expmul  8954  leexp2r  8962  leexp1a  8963  bernneq  9022  expnbnd  9025  cjth  9074  remim  9088  reim0b  9090  cjexp  9121  cnrecnv  9138