Theorem oveq1 5539

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

Assertion

Ref	Expression
oveq1	⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))

Proof of Theorem oveq1

Step	Hyp	Ref	Expression
1		opeq1 3570	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
2	1	fveq2d 5202	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘⟨𝐴, 𝐶⟩) = (𝐹‘⟨𝐵, 𝐶⟩))
3		df-ov 5535	. 2 ⊢ (𝐴𝐹𝐶) = (𝐹‘⟨𝐴, 𝐶⟩)
4		df-ov 5535	. 2 ⊢ (𝐵𝐹𝐶) = (𝐹‘⟨𝐵, 𝐶⟩)
5	2, 3, 4	3eqtr4g 2138	1 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))

Syntax hints:   → wi 4   = wceq 1284  ⟨cop 3401  ‘cfv 4922  (class class class)co 5532

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-3an 921  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-rex 2354  df-v 2603  df-un 2977  df-sn 3404  df-pr 3405  df-op 3407  df-uni 3602  df-br 3786  df-iota 4887  df-fv 4930  df-ov 5535

This theorem is referenced by:  oveq12  5541  oveq1i  5542  oveq1d  5547  rspceov  5567  fovcl  5626  ovmpt2s  5644  ov2gf  5645  ovi3  5657  caovclg  5673  caovcomg  5676  caovassg  5679  caovcang  5682  caovcan  5685  caovordig  5686  caovordg  5688  caovord  5692  caovdig  5695  caovdirg  5698  caovimo  5714  grpridd  5717  suppssov1  5729  off  5744  omcl  6064  oeicl  6065  omv2  6068  nnm0r  6081  nnacom  6086  nndi  6088  nnmass  6089  nnmsucr  6090  nnmcom  6091  nnaword  6107  nnmord  6113  nnm00  6125  eroveu  6220  th3qlem2  6232  th3q  6234  ecovcom  6236  ecovicom  6237  ecovass  6238  ecoviass  6239  ecovdi  6240  ecovidi  6241  addcmpblnq  6557  addclnq  6565  mulclnq  6566  mulidnq  6579  recexnq  6580  recmulnqg  6581  ltanqg  6590  ltmnqg  6591  ltexnqq  6598  enq0ref  6623  enq0tr  6624  addcmpblnq0  6633  mulnnnq0  6640  addclnq0  6641  mulclnq0  6642  distrnq0  6649  mulcomnq0  6650  addassnq0  6652  prarloclemlo  6684  prarloclem3  6687  prarloclem5  6690  prarloclemcalc  6692  genipv  6699  genpassl  6714  genpassu  6715  addlocprlemeq  6723  distrlem4prl  6774  distrlem4pru  6775  ltexprlemdisj  6796  ltexprlemloc  6797  ltexprlemrl  6800  ltexprlemru  6802  prplnqu  6810  cauappcvgprlemm  6835  cauappcvgprlemopl  6836  cauappcvgprlemlol  6837  cauappcvgprlemdisj  6841  cauappcvgprlemloc  6842  cauappcvgprlemladdfl  6845  cauappcvgprlemladdru  6846  cauappcvgprlemladdrl  6847  cauappcvgprlem1  6849  cauappcvgprlemlim  6851  cauappcvgpr  6852  caucvgprlemm  6858  caucvgprlemopl  6859  caucvgprlemlol  6860  caucvgprlemdisj  6864  caucvgprlemloc  6865  caucvgprlemladdrl  6868  caucvgprlem1  6869  caucvgpr  6872  caucvgprprlemell  6875  caucvgprprlemml  6884  caucvgprpr  6902  mulcmpblnrlemg  6917  addclsr  6930  mulclsr  6931  0idsr  6944  1idsr  6945  00sr  6946  ltasrg  6947  recexgt0sr  6950  mulgt0sr  6954  mulextsr1  6957  prsrriota  6964  caucvgsrlemgt1  6971  caucvgsrlemoffres  6976  pitonn  7016  peano2nnnn  7021  axaddrcl  7033  axmulrcl  7035  axaddcom  7036  ax1rid  7043  ax0id  7044  axprecex  7046  axcnre  7047  axpre-ltadd  7052  axpre-mulgt0  7053  axpre-mulext  7054  rereceu  7055  peano5nnnn  7058  axcaucvglemcau  7064  axcaucvglemres  7065  mulid1  7116  cnegexlem1  7283  cnegexlem2  7284  cnegex  7286  addcan2  7289  subval  7300  addlsub  7474  apreim  7703  recexap  7743  receuap  7759  divvalap  7762  cju  8038  peano2nn  8051  nn1m1nn  8057  nn1suc  8058  nnsub  8077  nnm1nn0  8329  zdiv  8435  zneo  8448  nneoor  8449  zeo  8452  peano5uzti  8455  nn0ind-raph  8464  uzind4s  8678  uzind4s2  8679  qmulz  8708  cnref1o  8733  nn0ledivnn  8838  fzsuc2  9096  fzm1  9117  fzoval  9158  qbtwnzlemstep  9257  qbtwnzlemshrink  9258  qbtwnzlemex  9259  qbtwnz  9260  rebtwn2zlemstep  9261  rebtwn2zlemshrink  9262  rebtwn2z  9263  flqlelt  9278  flqbi  9292  fldiv4p1lem1div2  9307  modqval  9326  modqadd1  9363  modqmuladd  9368  modqmuladdnn0  9370  modqm1p1mod0  9377  modqmul1  9379  modfzo0difsn  9397  addmodlteq  9400  frec2uzzd  9402  frec2uzsucd  9403  frec2uzrand  9407  frecuzrdgrrn  9410  frec2uzrdg  9411  frecuzrdgsuc  9417  uzsinds  9428  iseqval  9440  iseqp1  9445  iseqss  9446  iseqfveq2  9448  iseqshft2  9452  monoord  9455  monoord2  9456  iseqsplit  9458  iseqcaopr3  9460  iseqcaopr2  9461  iseqhomo  9468  iseqz  9469  iseqdistr  9470  m1expcl2  9498  mulexp  9515  expadd  9518  expmul  9521  sq0i  9567  sqoddm1div8  9625  facp1  9657  faclbnd  9668  faclbnd3  9670  bcval  9676  bcn1  9685  ibcval5  9690  bcpasc  9693  bccl  9694  shftlem  9704  shftfvalg  9706  shftfibg  9708  shftfval  9709  shftfib  9711  shftfn  9712  shftf  9718  2shfti  9719  shftvalg  9724  shftval4g  9725  cjval  9732  imval  9737  cjexp  9780  cnrecnv  9797  cvg1nlemcau  9870  cvg1nlemres  9871  resqrexlemcalc3  9902  resqrexlemex  9911  rsqrmo  9913  resqrtcl  9915  rersqrtthlem  9916  sqrtsq  9930  absexp  9965  recan  9995  climshft  10143  climcn1  10147  climcn2  10148  subcn2  10150  serif0  10189  dvdsval2  10198  dvds0lem  10205  dvds1lem  10206  dvds2lem  10207  dvdsmulc  10223  divconjdvds  10249  odd2np1lem  10271  odd2np1  10272  ltoddhalfle  10293  halfleoddlt  10294  nn0o1gt2  10305  nn0o  10307  divalglemnn  10318  divalglemeunn  10321  divalglemex  10322  divalglemeuneg  10323  flodddiv4  10334  gcdabs1  10380  gcddiv  10408  dvdssqim  10413  rpmulgcd  10415  bezoutr1  10422  dvdslcm  10451  lcmeq0  10453  lcmdvds  10461  divgcdcoprm0  10483  prmind2  10502  isprm6  10526  rpexp  10532  sqrt2irr  10541  pw2dvdslemn  10543  pw2dvdseu  10546  oddpwdclemxy  10547  qdencn  10785