Theorem oveq1 5860

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 3765	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
2	1	fveq2d 5500	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘⟨𝐴, 𝐶⟩) = (𝐹‘⟨𝐵, 𝐶⟩))
3		df-ov 5856	. 2 ⊢ (𝐴𝐹𝐶) = (𝐹‘⟨𝐴, 𝐶⟩)
4		df-ov 5856	. 2 ⊢ (𝐵𝐹𝐶) = (𝐹‘⟨𝐵, 𝐶⟩)
5	2, 3, 4	3eqtr4g 2228	1 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))

Syntax hints:   → wi 4   = wceq 1348  ⟨cop 3586  ‘cfv 5198  (class class class)co 5853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-rex 2454  df-v 2732  df-un 3125  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-br 3990  df-iota 5160  df-fv 5206  df-ov 5856

This theorem is referenced by:  oveq12  5862  oveq1i  5863  oveq1d  5868  ovrspc2v  5879  oveqrspc2v  5880  rspceov  5895  fovcl  5958  ovmpos  5976  ov2gf  5977  ovi3  5989  caovclg  6005  caovcomg  6008  caovassg  6011  caovcang  6014  caovcan  6017  caovordig  6018  caovordg  6020  caovord  6024  caovdig  6027  caovdirg  6030  caovimo  6046  suppssov1  6058  off  6073  omcl  6440  oeicl  6441  omv2  6444  nnm0r  6458  nnacom  6463  nndi  6465  nnmass  6466  nnmsucr  6467  nnmcom  6468  nnaword  6490  nnmord  6496  nnm00  6509  eroveu  6604  th3qlem2  6616  th3q  6618  ecovcom  6620  ecovicom  6621  ecovass  6622  ecoviass  6623  ecovdi  6624  ecovidi  6625  map0g  6666  addcmpblnq  7329  addclnq  7337  mulclnq  7338  mulidnq  7351  recexnq  7352  recmulnqg  7353  ltanqg  7362  ltmnqg  7363  ltexnqq  7370  enq0ref  7395  enq0tr  7396  addcmpblnq0  7405  mulnnnq0  7412  addclnq0  7413  mulclnq0  7414  distrnq0  7421  mulcomnq0  7422  addassnq0  7424  prarloclemlo  7456  prarloclem3  7459  prarloclem5  7462  prarloclemcalc  7464  genipv  7471  genpassl  7486  genpassu  7487  addlocprlemeq  7495  distrlem4prl  7546  distrlem4pru  7547  ltexprlemdisj  7568  ltexprlemloc  7569  ltexprlemrl  7572  ltexprlemru  7574  prplnqu  7582  cauappcvgprlemm  7607  cauappcvgprlemopl  7608  cauappcvgprlemlol  7609  cauappcvgprlemdisj  7613  cauappcvgprlemloc  7614  cauappcvgprlemladdfl  7617  cauappcvgprlemladdru  7618  cauappcvgprlemladdrl  7619  cauappcvgprlem1  7621  cauappcvgprlemlim  7623  cauappcvgpr  7624  caucvgprlemm  7630  caucvgprlemopl  7631  caucvgprlemlol  7632  caucvgprlemdisj  7636  caucvgprlemloc  7637  caucvgprlemladdrl  7640  caucvgprlem1  7641  caucvgpr  7644  caucvgprprlemell  7647  caucvgprprlemml  7656  caucvgprpr  7674  mulcmpblnrlemg  7702  addclsr  7715  mulclsr  7716  0idsr  7729  1idsr  7730  00sr  7731  ltasrg  7732  recexgt0sr  7735  mulgt0sr  7740  mulextsr1  7743  prsrriota  7750  caucvgsrlemgt1  7757  caucvgsrlemoffres  7762  pitonn  7810  peano2nnnn  7815  axaddrcl  7827  axmulrcl  7829  axaddcom  7832  ax1rid  7839  ax0id  7840  axprecex  7842  axcnre  7843  axpre-ltadd  7848  axpre-mulgt0  7849  axpre-mulext  7850  rereceu  7851  peano5nnnn  7854  axcaucvglemcau  7860  axcaucvglemres  7861  mulid1  7917  cnegexlem1  8094  cnegexlem2  8095  cnegex  8097  addcan2  8100  subval  8111  addlsub  8289  apreim  8522  recexap  8571  receuap  8587  divvalap  8591  cju  8877  peano2nn  8890  nn1m1nn  8896  nn1suc  8897  nnsub  8917  fv0p1e1  8993  nnm1nn0  9176  zdiv  9300  zneo  9313  nneoor  9314  zeo  9317  peano5uzti  9320  nn0ind-raph  9329  uzind4s  9549  uzind4s2  9550  qmulz  9582  elpq  9607  cnref1o  9609  nn0ledivnn  9724  xaddnemnf  9814  xaddnepnf  9815  xaddcom  9818  xaddid1  9819  xnn0xadd0  9824  xaddass  9826  xpncan  9828  xleadd1a  9830  xltadd1  9833  xlt2add  9837  xsubge0  9838  xposdif  9839  xlesubadd  9840  xleaddadd  9844  fzsuc2  10035  fzm1  10056  fzoval  10104  exbtwnzlemstep  10204  exbtwnzlemshrink  10205  exbtwnzlemex  10206  exbtwnz  10207  rebtwn2zlemstep  10209  rebtwn2zlemshrink  10210  rebtwn2z  10211  flqlelt  10232  flqbi  10246  fldiv4p1lem1div2  10261  modqval  10280  modqadd1  10317  modqmuladd  10322  modqmuladdnn0  10324  modqm1p1mod0  10331  modqmul1  10333  modfzo0difsn  10351  addmodlteq  10354  frec2uzzd  10356  frec2uzsucd  10357  frec2uzrand  10361  frecuzrdgrrn  10364  frec2uzrdg  10365  frecuzrdgrcl  10366  frecuzrdgsuc  10370  frecuzrdgrclt  10371  frecuzrdgg  10372  frecuzrdgdom  10374  frecuzrdgfun  10376  frecuzrdgsuctlem  10379  frecuzrdgsuct  10380  uzsinds  10398  iseqvalcbv  10413  seq3val  10414  seqvalcd  10415  seqf  10417  seq3p1  10418  seqovcd  10419  seqp1cd  10422  seq3fveq2  10425  seq3shft2  10429  monoord  10432  monoord2  10433  seq3split  10435  seq3caopr3  10437  seq3caopr2  10438  iseqf1olemqval  10443  iseqf1olemqk  10450  seq3id2  10465  seq3homo  10466  seq3z  10467  seq3distr  10469  m1expcl2  10498  mulexp  10515  expadd  10518  expmul  10521  sq0i  10567  qsqeqor  10586  sqoddm1div8  10629  facp1  10664  faclbnd  10675  faclbnd3  10677  bcval  10683  bcn1  10692  bcval5  10697  bcpasc  10700  bccl  10701  hashfz1  10717  omgadd  10737  hashfzo  10757  hashfzp1  10759  hashxp  10761  seq3coll  10777  shftlem  10780  shftfvalg  10782  shftfibg  10784  shftfval  10785  shftfib  10787  shftfn  10788  shftf  10794  2shfti  10795  shftvalg  10800  shftval4g  10801  cjval  10809  imval  10814  cjexp  10857  cnrecnv  10874  cvg1nlemcau  10948  cvg1nlemres  10949  resqrexlemcalc3  10980  resqrexlemex  10989  rsqrmo  10991  resqrtcl  10993  rersqrtthlem  10994  sqrtsq  11008  absexp  11043  recan  11073  climshft  11267  climcn1  11271  climcn2  11272  subcn2  11274  fsumshft  11407  fisum0diag2  11410  fsumiun  11440  binomlem  11446  binom  11447  bcxmas  11452  isumsplit  11454  arisum2  11462  trireciplem  11463  trirecip  11464  geolim  11474  cvgratnnlemnexp  11487  cvgratnnlemmn  11488  clim2prod  11502  prodfrecap  11509  fprodcl2lem  11568  fprodfac  11578  fprodshft  11581  ef0lem  11623  efval  11624  efne0  11641  efexp  11645  demoivreALT  11736  dvdsval2  11752  p1modz1  11756  dvds0lem  11763  dvds1lem  11764  dvds2lem  11765  dvdsmulc  11781  divconjdvds  11809  odd2np1lem  11831  odd2np1  11832  ltoddhalfle  11852  halfleoddlt  11853  nn0o1gt2  11864  nn0o  11866  divalglemnn  11877  divalglemeunn  11880  divalglemex  11881  divalglemeuneg  11882  flodddiv4  11893  gcdabs1  11944  gcddiv  11974  dvdssqim  11979  rpmulgcd  11981  bezoutr1  11988  uzwodc  11992  dvdslcm  12023  lcmeq0  12025  lcmdvds  12033  divgcdcoprm0  12055  prmind2  12074  isprm5lem  12095  isprm6  12101  rpexp  12107  sqrt2irr  12116  pw2dvdslemn  12119  pw2dvdseu  12122  oddpwdclemxy  12123  nn0gcdsq  12154  phicl2  12168  phibndlem  12170  hashdvds  12175  crth  12178  phimullem  12179  eulerthlem1  12181  eulerthlemfi  12182  eulerthlemrprm  12183  eulerthlemth  12186  eulerth  12187  hashgcdlem  12192  phisum  12194  odzval  12195  modprm0  12208  nnnn0modprm0  12209  pythagtriplem1  12219  pythagtriplem6  12224  pythagtriplem7  12225  pythagtriplem12  12229  pythagtriplem14  12231  pythagtriplem18  12235  pythagtriplem19  12236  pceulem  12248  pceu  12249  pcval  12250  pczpre  12251  pcdiv  12256  pcqmul  12257  pcqcl  12260  pcexp  12263  pcaddlem  12292  pcadd  12293  pcmpt  12295  pcprod  12298  pcfac  12302  expnprm  12305  prmpwdvds  12307  pockthi  12310  1arithlem2  12316  4sqlem2  12341  4sqlem3  12342  ennnfonelemr  12378  ctinfom  12383  infpn2  12411  mgm1  12624  mgmidmo  12626  ismgmid  12631  mgmlrid  12633  ismgmid2  12634  lidrideqd  12635  lidrididd  12636  mgmidsssn0  12638  grpridd  12641  isnsgrp  12647  sgrpass  12649  sgrp1  12651  sgrpidmndm  12656  ismndd  12673  mndinvmod  12678  mnd1  12679  mnd1id  12680  mhmpropd  12689  insubm  12703  mhmima  12706  grppropd  12724  isgrpd2  12727  isgrpd  12729  dfgrp2  12732  grprcan  12740  grpinveu  12741  grpsubval  12749  grplinv  12752  grpinvid2  12755  isgrpinv  12756  grplrinv  12757  grpidinv2  12758  grpidinv  12759  cnmptcom  13092  psmettri2  13122  isxmet2d  13142  xmeteq0  13153  xmettri2  13155  metrest  13300  cncfval  13353  mulc1cncf  13370  addccncf  13380  mulcncf  13385  expcncf  13386  limccnp2lem  13439  dvcnp2cntop  13457  dvcoapbr  13465  dvexp  13469  dvrecap  13471  dvef  13482  sincn  13484  coscn  13485  ptolemy  13539  sincosq1eq  13554  logbgcd1irr  13679  logbgcd1irraplemexp  13680  2irrexpq  13688  2irrexpqap  13690  lgslem4  13698  lgsval  13699  lgsfvalg  13700  lgsval2lem  13705  lgsdir2lem4  13726  lgsdir  13730  lgsdilem2  13731  lgsdi  13732  lgsne0  13733  lgsmodeq  13740  lgsdirnn0  13742  lgsdinn0  13743  2sqlem2  13745  2sqlem6  13750  2sqlem8  13753  2sqlem9  13754  qdencn  14059  isomninn  14063  trirec0  14076  iswomninn  14082  ismkvnn  14085