Theorem oveq2 5520

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 3550	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
2	1	fveq2d 5182	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘⟨𝐶, 𝐴⟩) = (𝐹‘⟨𝐶, 𝐵⟩))
3		df-ov 5515	. 2 ⊢ (𝐶𝐹𝐴) = (𝐹‘⟨𝐶, 𝐴⟩)
4		df-ov 5515	. 2 ⊢ (𝐶𝐹𝐵) = (𝐹‘⟨𝐶, 𝐵⟩)
5	2, 3, 4	3eqtr4g 2097	1 ⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))

Syntax hints:   → wi 4   = wceq 1243  ⟨cop 3378  ‘cfv 4902  (class class class)co 5512

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 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-rex 2312  df-v 2559  df-un 2922  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-br 3765  df-iota 4867  df-fv 4910  df-ov 5515

This theorem is referenced by:  oveq12  5521  oveq2i  5523  oveq2d  5528  rspceov  5547  fovcl  5606  ovmpt2s  5624  ov2gf  5625  ovi3  5637  caovclg  5653  caovcomg  5656  caovassg  5659  caovcang  5662  caovcan  5665  caovordig  5666  caovordg  5668  caovord  5672  caovdig  5675  caovdirg  5678  caovimo  5694  grprinvlem  5695  grprinvd  5696  suppssov1  5709  off  5724  omv  6035  oeiv  6036  oasuc  6044  omsuc  6051  nna0r  6057  nnm0r  6058  nnacl  6059  nnmcl  6060  nnacom  6063  nnaass  6064  nndi  6065  nnmass  6066  nnmsucr  6067  nnmcom  6068  nnaordi  6081  nnaord  6082  nnmordi  6089  nnmord  6090  nnaordex  6100  nnawordex  6101  nnm00  6102  eroveu  6197  ecopovtrn  6203  ecopovtrng  6206  th3qlem2  6209  th3q  6211  ecovcom  6213  ecovicom  6214  ecovass  6215  ecoviass  6216  ecovdi  6217  ecovidi  6218  addcanpig  6432  mulcanpig  6433  addcmpblnq  6465  addclnq  6473  mulclnq  6474  recexnq  6488  recmulnqg  6489  ltanqg  6498  ltmnqg  6499  ltexnqq  6506  enq0ref  6531  enq0tr  6532  addcmpblnq0  6541  mulnnnq0  6548  addclnq0  6549  mulclnq0  6550  distrnq0  6557  mulcomnq0  6558  addassnq0  6560  nq02m  6563  prarloclem3  6595  genipv  6607  genpassl  6622  genpassu  6623  addlocpr  6634  distrlem1prl  6680  distrlem1pru  6681  1idprl  6688  1idpru  6689  ltexprlemell  6696  ltexprlemelu  6697  ltexpri  6711  lteupri  6715  ltaprlem  6716  recexprlem1ssl  6731  recexprlem1ssu  6732  recexpr  6736  cauappcvgprlemm  6743  cauappcvgprlemdisj  6749  cauappcvgprlemloc  6750  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  cauappcvgprlem1  6757  cauappcvgprlemlim  6759  cauappcvgpr  6760  mulcmpblnrlemg  6825  addclsr  6838  mulclsr  6839  ltasrg  6855  negexsr  6857  recexgt0sr  6858  mulgt0sr  6862  mulextsr1  6865  srpospr  6867  caucvgsrlemgt1  6879  axaddrcl  6941  axmulrcl  6943  axaddcom  6944  axrnegex  6953  axprecex  6954  axcnre  6955  axpre-ltadd  6960  axpre-mulgt0  6961  axpre-mulext  6962  rereceu  6963  recriota  6964  axcaucvglemres  6973  readdcan  7153  cnegexlem1  7186  cnegex  7189  addcan  7191  negeq  7204  subadd  7214  ine0  7391  rimul  7576  cru  7593  apreim  7594  recexap  7634  mulcanapd  7642  receuap  7650  divmulap  7654  cju  7913  nnaddcl  7934  nnmulcl  7935  nnsub  7952  nnnn0addcl  8212  zaddcllempos  8282  zaddcl  8285  zdiv  8328  deceq1  8370  deceq2  8371  uzaddcl  8529  zq  8561  qreccl  8576  cnref1o  8582  fzsuc2  8941  fzrevral  8967  fzshftral  8970  2ffzeq  8998  qbtwnzlemshrink  9104  rebtwn2zlemshrink  9108  modqval  9166  frecuzrdgrrn  9194  frec2uzrdg  9195  frecuzrdgsuc  9201  frecfzennn  9203  iseqcaopr3  9240  iseqcaopr2  9241  iseqid  9247  iseqhomo  9248  iseqdistr  9249  expp1  9262  expnegap0  9263  expcllem  9266  expcl2lemap  9267  m1expcl2  9277  expap0  9285  mulexp  9294  expadd  9297  expmul  9300  leexp2r  9308  leexp1a  9309  bernneq  9369  expnbnd  9372  shftfvalg  9419  shftfval  9422  cjth  9446  remim  9460  reim0b  9462  cjexp  9493  cnrecnv  9510  cvg1nlemcau  9583  cvg1nlemres  9584  recvguniq  9593  resqrexlemp1rp  9604  resqrexlemfp1  9607  resqrexlemlo  9611  resqrexlemgt0  9618  resqrexlemoverl  9619  resqrexlemglsq  9620  resqrexlemsqa  9622  resqrexlemex  9623  resqrex  9624  absexp  9675  recan  9705  climcn2  9830  subcn2  9832  sqrt2irr  9878  nn0seqcvgd  9880