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-bnd 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  6415  enq0tr  6416  addcmpblnq0  6425  mulnnnq0  6432  addclnq0  6433  mulclnq0  6434  distrnq0  6441  mulcomnq0  6442  addassnq0  6444  nq02m  6447  prarloclem3  6479  genipv  6491  genpassl  6506  genpassu  6507  addlocpr  6518  distrlem1prl  6557  distrlem1pru  6558  1idprl  6565  1idpru  6566  ltexprlemell  6571  ltexprlemelu  6572  ltexpri  6586  ltaprlem  6590  recexprlem1ssl  6604  recexprlem1ssu  6605  recexpr  6609  cauappcvgprlemm  6616  cauappcvgprlemdisj  6622  cauappcvgprlemloc  6623  cauappcvgprlemladdru  6627  cauappcvgprlemladdrl  6628  cauappcvgprlem1  6630  cauappcvgprlemlim  6632  cauappcvgpr  6633  mulcmpblnrlemg  6648  addclsr  6661  mulclsr  6662  ltasrg  6678  negexsr  6680  recexgt0sr  6681  mulgt0sr  6684  mulextsr1  6687  axaddrcl  6731  axmulrcl  6733  axaddcom  6734  axrnegex  6743  axprecex  6744  axcnre  6745  axpre-ltadd  6750  axpre-mulgt0  6751  axpre-mulext  6752  readdcan  6930  cnegexlem1  6963  cnegex  6966  addcan  6968  negeq  6981  subadd  6991  ine0  7167  rimul  7349  cru  7366  apreim  7367  recexap  7396  mulcanapd  7404  receuap  7412  divmulap  7416  cju  7674  nnaddcl  7695  nnmulcl  7696  nnsub  7713  nnnn0addcl  7968  zaddcllempos  8038  zaddcl  8041  zdiv  8084  deceq1  8126  deceq2  8127  uzaddcl  8285  zq  8317  qreccl  8331  cnref1o  8337  fzsuc2  8691  fzrevral  8717  fzshftral  8720  2ffzeq  8748  frecuzrdgrrn  8855  frec2uzrdg  8856  frecuzrdgsuc  8862  frecfzennn  8864  expp1  8896  expnegap0  8897  expcllem  8900  expcl2lemap  8901  m1expcl2  8911  expap0  8919  mulexp  8928  expadd  8931  expmul  8934  leexp2r  8942  leexp1a  8943  bernneq  9002  expnbnd  9005  cjth  9054  remim  9068  reim0b  9070  cjexp  9101  cnrecnv  9118