Theorem oveq2 5460

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 3540	. . 3 ⊢ (A = B → ⟨𝐶, A⟩ = ⟨𝐶, B⟩)
2	1	fveq2d 5123	. 2 ⊢ (A = B → (𝐹‘⟨𝐶, A⟩) = (𝐹‘⟨𝐶, B⟩))
3		df-ov 5455	. 2 ⊢ (𝐶𝐹A) = (𝐹‘⟨𝐶, A⟩)
4		df-ov 5455	. 2 ⊢ (𝐶𝐹B) = (𝐹‘⟨𝐶, B⟩)
5	2, 3, 4	3eqtr4g 2094	1 ⊢ (A = B → (𝐶𝐹A) = (𝐶𝐹B))

Syntax hints:   → wi 4   = wceq 1242  ⟨cop 3369  ‘cfv 4844  (class class class)co 5452

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 3372  df-pr 3373  df-op 3375  df-uni 3571  df-br 3755  df-iota 4809  df-fv 4852  df-ov 5455

This theorem is referenced by:  oveq12  5461  oveq2i  5463  oveq2d  5468  rspceov  5486  fovcl  5545  ovmpt2s  5563  ov2gf  5564  ovi3  5576  caovclg  5592  caovcomg  5595  caovassg  5598  caovcang  5601  caovcan  5604  caovordig  5605  caovordg  5607  caovord  5611  caovdig  5614  caovdirg  5617  caovimo  5633  grprinvlem  5634  grprinvd  5635  suppssov1  5648  off  5663  omv  5967  oeiv  5968  oasuc  5976  omsuc  5983  nna0r  5989  nnm0r  5990  nnacl  5991  nnmcl  5992  nnacom  5995  nnaass  5996  nndi  5997  nnmass  5998  nnmsucr  5999  nnmcom  6000  nnaordi  6010  nnaord  6011  nnmordi  6018  nnmord  6019  nnaordex  6029  nnawordex  6030  nnm00  6031  eroveu  6126  ecopovtrn  6132  ecopovtrng  6135  th3qlem2  6138  th3q  6140  ecovcom  6142  ecovicom  6143  ecovass  6144  ecoviass  6145  ecovdi  6146  ecovidi  6147  addcanpig  6311  mulcanpig  6312  addcmpblnq  6344  addclnq  6352  mulclnq  6353  recexnq  6367  recmulnqg  6368  ltanqg  6377  ltmnqg  6378  ltexnqq  6384  enq0ref  6408  enq0tr  6409  addcmpblnq0  6418  mulnnnq0  6425  addclnq0  6426  mulclnq0  6427  distrnq0  6434  mulcomnq0  6435  addassnq0  6437  nq02m  6440  prarloclem3  6472  genipv  6484  genpassl  6500  genpassu  6501  addlocpr  6512  distrlem1prl  6548  distrlem1pru  6549  1idprl  6556  1idpru  6557  ltexprlemell  6562  ltexprlemelu  6563  ltexpri  6577  ltaprlem  6581  recexprlem1ssl  6595  recexprlem1ssu  6596  recexpr  6600  mulcmpblnrlemg  6620  addclsr  6633  mulclsr  6634  ltasrg  6650  negexsr  6652  recexgt0sr  6653  mulgt0sr  6656  mulextsr1  6659  axaddrcl  6703  axmulrcl  6705  axaddcom  6706  axrnegex  6715  axprecex  6716  axcnre  6717  axpre-ltadd  6722  axpre-mulgt0  6723  axpre-mulext  6724  readdcan  6902  cnegexlem1  6935  cnegex  6938  addcan  6940  negeq  6953  subadd  6963  ine0  7139  rimul  7321  cru  7338  apreim  7339  recexap  7368  mulcanapd  7376  receuap  7384  divmulap  7388  cju  7645  nnaddcl  7666  nnmulcl  7667  nnsub  7684  nnnn0addcl  7938  zaddcllempos  8008  zaddcl  8011  zdiv  8053  deceq1  8095  deceq2  8096  uzaddcl  8254  zq  8286  qreccl  8300  fzsuc2  8657  fzrevral  8683  fzshftral  8686  2ffzeq  8714  frecfzennn  8822