Theorem oveq1 5895

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 3790	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
2	1	fveq2d 5531	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘⟨𝐴, 𝐶⟩) = (𝐹‘⟨𝐵, 𝐶⟩))
3		df-ov 5891	. 2 ⊢ (𝐴𝐹𝐶) = (𝐹‘⟨𝐴, 𝐶⟩)
4		df-ov 5891	. 2 ⊢ (𝐵𝐹𝐶) = (𝐹‘⟨𝐵, 𝐶⟩)
5	2, 3, 4	3eqtr4g 2245	1 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))

Syntax hints:   → wi 4   = wceq 1363  ⟨cop 3607  ‘cfv 5228  (class class class)co 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-3an 981  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-rex 2471  df-v 2751  df-un 3145  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-br 4016  df-iota 5190  df-fv 5236  df-ov 5891

This theorem is referenced by:  oveq12  5897  oveq1i  5898  oveq1d  5903  ovrspc2v  5914  oveqrspc2v  5915  rspceov  5930  fovcld  5993  ovmpos  6012  ov2gf  6013  ovi3  6025  caovclg  6041  caovcomg  6044  caovassg  6047  caovcang  6050  caovcan  6053  caovordig  6054  caovordg  6056  caovord  6060  caovdig  6063  caovdirg  6066  caovimo  6082  suppssov1  6094  off  6109  omcl  6476  oeicl  6477  omv2  6480  nnm0r  6494  nnacom  6499  nndi  6501  nnmass  6502  nnmsucr  6503  nnmcom  6504  nnaword  6526  nnmord  6532  nnm00  6545  eroveu  6640  th3qlem2  6652  th3q  6654  ecovcom  6656  ecovicom  6657  ecovass  6658  ecoviass  6659  ecovdi  6660  ecovidi  6661  map0g  6702  addcmpblnq  7380  addclnq  7388  mulclnq  7389  mulidnq  7402  recexnq  7403  recmulnqg  7404  ltanqg  7413  ltmnqg  7414  ltexnqq  7421  enq0ref  7446  enq0tr  7447  addcmpblnq0  7456  mulnnnq0  7463  addclnq0  7464  mulclnq0  7465  distrnq0  7472  mulcomnq0  7473  addassnq0  7475  prarloclemlo  7507  prarloclem3  7510  prarloclem5  7513  prarloclemcalc  7515  genipv  7522  genpassl  7537  genpassu  7538  addlocprlemeq  7546  distrlem4prl  7597  distrlem4pru  7598  ltexprlemdisj  7619  ltexprlemloc  7620  ltexprlemrl  7623  ltexprlemru  7625  prplnqu  7633  cauappcvgprlemm  7658  cauappcvgprlemopl  7659  cauappcvgprlemlol  7660  cauappcvgprlemdisj  7664  cauappcvgprlemloc  7665  cauappcvgprlemladdfl  7668  cauappcvgprlemladdru  7669  cauappcvgprlemladdrl  7670  cauappcvgprlem1  7672  cauappcvgprlemlim  7674  cauappcvgpr  7675  caucvgprlemm  7681  caucvgprlemopl  7682  caucvgprlemlol  7683  caucvgprlemdisj  7687  caucvgprlemloc  7688  caucvgprlemladdrl  7691  caucvgprlem1  7692  caucvgpr  7695  caucvgprprlemell  7698  caucvgprprlemml  7707  caucvgprpr  7725  mulcmpblnrlemg  7753  addclsr  7766  mulclsr  7767  0idsr  7780  1idsr  7781  00sr  7782  ltasrg  7783  recexgt0sr  7786  mulgt0sr  7791  mulextsr1  7794  prsrriota  7801  caucvgsrlemgt1  7808  caucvgsrlemoffres  7813  pitonn  7861  peano2nnnn  7866  axaddrcl  7878  axmulrcl  7880  axaddcom  7883  ax1rid  7890  ax0id  7891  axprecex  7893  axcnre  7894  axpre-ltadd  7899  axpre-mulgt0  7900  axpre-mulext  7901  rereceu  7902  peano5nnnn  7905  axcaucvglemcau  7911  axcaucvglemres  7912  mulrid  7968  cnegexlem1  8146  cnegexlem2  8147  cnegex  8149  addcan2  8152  subval  8163  addlsub  8341  apreim  8574  recexap  8624  receuap  8640  divvalap  8645  cju  8932  peano2nn  8945  nn1m1nn  8951  nn1suc  8952  nnsub  8972  fv0p1e1  9048  nnm1nn0  9231  zdiv  9355  zneo  9368  nneoor  9369  zeo  9372  peano5uzti  9375  nn0ind-raph  9384  uzind4s  9604  uzind4s2  9605  qmulz  9637  elpq  9662  cnref1o  9664  nn0ledivnn  9781  xaddnemnf  9871  xaddnepnf  9872  xaddcom  9875  xaddid1  9876  xnn0xadd0  9881  xaddass  9883  xpncan  9885  xleadd1a  9887  xltadd1  9890  xlt2add  9894  xsubge0  9895  xposdif  9896  xlesubadd  9897  xleaddadd  9901  fzsuc2  10093  fzm1  10114  fzoval  10162  exbtwnzlemstep  10262  exbtwnzlemshrink  10263  exbtwnzlemex  10264  exbtwnz  10265  rebtwn2zlemstep  10267  rebtwn2zlemshrink  10268  rebtwn2z  10269  flqlelt  10290  flqbi  10304  fldiv4p1lem1div2  10319  modqval  10338  modqadd1  10375  modqmuladd  10380  modqmuladdnn0  10382  modqm1p1mod0  10389  modqmul1  10391  modfzo0difsn  10409  addmodlteq  10412  frec2uzzd  10414  frec2uzsucd  10415  frec2uzrand  10419  frecuzrdgrrn  10422  frec2uzrdg  10423  frecuzrdgrcl  10424  frecuzrdgsuc  10428  frecuzrdgrclt  10429  frecuzrdgg  10430  frecuzrdgdom  10432  frecuzrdgfun  10434  frecuzrdgsuctlem  10437  frecuzrdgsuct  10438  uzsinds  10456  iseqvalcbv  10471  seq3val  10472  seqvalcd  10473  seqf  10475  seq3p1  10476  seqovcd  10477  seqp1cd  10480  seq3fveq2  10483  seq3shft2  10487  monoord  10490  monoord2  10491  seq3split  10493  seq3caopr3  10495  seq3caopr2  10496  iseqf1olemqval  10501  iseqf1olemqk  10508  seq3id2  10523  seq3homo  10524  seq3z  10525  seq3distr  10527  m1expcl2  10556  mulexp  10573  expadd  10576  expmul  10579  sq0i  10626  qsqeqor  10645  sqoddm1div8  10688  facp1  10724  faclbnd  10735  faclbnd3  10737  bcval  10743  bcn1  10752  bcval5  10757  bcpasc  10760  bccl  10761  hashfz1  10777  omgadd  10796  hashfzo  10816  hashfzp1  10818  hashxp  10820  seq3coll  10836  shftlem  10839  shftfvalg  10841  shftfibg  10843  shftfval  10844  shftfib  10846  shftfn  10847  shftf  10853  2shfti  10854  shftvalg  10859  shftval4g  10860  cjval  10868  imval  10873  cjexp  10916  cnrecnv  10933  cvg1nlemcau  11007  cvg1nlemres  11008  resqrexlemcalc3  11039  resqrexlemex  11048  rsqrmo  11050  resqrtcl  11052  rersqrtthlem  11053  sqrtsq  11067  absexp  11102  recan  11132  climshft  11326  climcn1  11330  climcn2  11331  subcn2  11333  fsumshft  11466  fisum0diag2  11469  fsumiun  11499  binomlem  11505  binom  11506  bcxmas  11511  isumsplit  11513  arisum2  11521  trireciplem  11522  trirecip  11523  geolim  11533  cvgratnnlemnexp  11546  cvgratnnlemmn  11547  clim2prod  11561  prodfrecap  11568  fprodcl2lem  11627  fprodfac  11637  fprodshft  11640  ef0lem  11682  efval  11683  efne0  11700  efexp  11704  demoivreALT  11795  dvdsval2  11811  p1modz1  11815  dvds0lem  11822  dvds1lem  11823  dvds2lem  11824  dvdsmulc  11840  divconjdvds  11869  odd2np1lem  11891  odd2np1  11892  ltoddhalfle  11912  halfleoddlt  11913  nn0o1gt2  11924  nn0o  11926  divalglemnn  11937  divalglemeunn  11940  divalglemex  11941  divalglemeuneg  11942  flodddiv4  11953  gcdabs1  12004  gcddiv  12034  dvdssqim  12039  rpmulgcd  12041  bezoutr1  12048  uzwodc  12052  dvdslcm  12083  lcmeq0  12085  lcmdvds  12093  divgcdcoprm0  12115  prmind2  12134  isprm5lem  12155  isprm6  12161  rpexp  12167  sqrt2irr  12176  pw2dvdslemn  12179  pw2dvdseu  12182  oddpwdclemxy  12183  nn0gcdsq  12214  phicl2  12228  phibndlem  12230  hashdvds  12235  crth  12238  phimullem  12239  eulerthlem1  12241  eulerthlemfi  12242  eulerthlemrprm  12243  eulerthlemth  12246  eulerth  12247  hashgcdlem  12252  phisum  12254  odzval  12255  modprm0  12268  nnnn0modprm0  12269  pythagtriplem1  12279  pythagtriplem6  12284  pythagtriplem7  12285  pythagtriplem12  12289  pythagtriplem14  12291  pythagtriplem18  12295  pythagtriplem19  12296  pceulem  12308  pceu  12309  pcval  12310  pczpre  12311  pcdiv  12316  pcqmul  12317  pcqcl  12320  pcexp  12323  pcaddlem  12352  pcadd  12353  pcmpt  12355  pcprod  12358  pcfac  12362  expnprm  12365  prmpwdvds  12367  pockthi  12370  1arithlem2  12376  4sqlem2  12401  4sqlem3  12402  ennnfonelemr  12438  ctinfom  12443  infpn2  12471  ercpbl  12769  mgm1  12808  mgmidmo  12810  ismgmid  12815  mgmlrid  12817  ismgmid2  12818  lidrideqd  12819  lidrididd  12820  mgmidsssn0  12822  grprida  12825  isnsgrp  12831  sgrpass  12833  sgrp1  12836  sgrpidmndm  12843  ismndd  12860  mndinvmod  12868  mnd1  12869  mnd1id  12870  mhmpropd  12879  insubm  12898  mhmima  12904  grppropd  12923  isgrpd2  12927  isgrpd  12929  dfgrp2  12932  grprcan  12942  grpinveu  12943  grpsubval  12951  grplinv  12955  grpinvid2  12958  isgrpinv  12959  grplrinv  12962  grpidinv2  12963  grpidinv  12964  grpidssd  12981  grpinvssd  12982  dfgrp3mlem  13003  dfgrp3m  13004  grplactfval  13006  grp1  13011  imasgrp2  13013  mhmmnd  13019  ghmgrp  13021  mulgnn0p1  13034  mulgnn0subcl  13036  mulgaddcom  13047  mulginvcom  13048  mulgnn0z  13050  mulgneg2  13057  mulgnnass  13058  mulgnn0ass  13059  mhmmulg  13064  issubg  13073  subgex  13076  issubg2m  13089  issubg4m  13093  isnsg2  13103  nsgbi  13104  isnsg3  13107  elnmz  13108  nmzbi  13109  ghmrn  13151  ghmnsgima  13162  rngdi  13249  rngdir  13250  srgrz  13293  srgmulgass  13298  srgpcomp  13299  srgrmhm  13303  ringid  13335  ringinvnzdiv  13357  mulgass2  13365  ring1  13366  imasring  13369  dvdsrmuld  13401  dvdsrmul1  13407  dvdsr01  13409  dvreq1  13447  lringuplu  13473  issubrng  13476  issubrng2  13487  issubrg  13498  issubrg2  13518  lmodlema  13538  islmodd  13539  lmodvsmmulgdi  13569  rmodislmodlem  13596  rmodislmod  13597  lssclg  13610  lss1d  13629  lspsn  13662  sraval  13683  rnglidlmcl  13726  quscrng  13777  cnfldmulg  13809  cnfldexp  13810  zlmval  13842  cnmptcom  14151  psmettri2  14181  isxmet2d  14201  xmeteq0  14212  xmettri2  14214  metrest  14359  cncfval  14412  mulc1cncf  14429  addccncf  14439  mulcncf  14444  expcncf  14445  limccnp2lem  14498  dvcnp2cntop  14516  dvcoapbr  14524  dvexp  14528  dvrecap  14530  dvef  14541  sincn  14543  coscn  14544  ptolemy  14598  sincosq1eq  14613  logbgcd1irr  14738  logbgcd1irraplemexp  14739  2irrexpq  14747  2irrexpqap  14749  lgslem4  14757  lgsval  14758  lgsfvalg  14759  lgsval2lem  14764  lgsdir2lem4  14785  lgsdir  14789  lgsdilem2  14790  lgsdi  14791  lgsne0  14792  lgsmodeq  14799  lgsdirnn0  14801  lgsdinn0  14802  lgseisenlem2  14804  2lgsoddprmlem1  14806  2lgsoddprmlem3  14812  2sqlem2  14815  2sqlem6  14820  2sqlem8  14823  2sqlem9  14824  qdencn  15129  isomninn  15133  trirec0  15146  iswomninn  15152  ismkvnn  15155