Theorem oveq1 6092

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 3904	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
2	1	fveq2d 5699	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘⟨𝐴, 𝐶⟩) = (𝐹‘⟨𝐵, 𝐶⟩))
3		df-ov 6088	. 2 ⊢ (𝐴𝐹𝐶) = (𝐹‘⟨𝐴, 𝐶⟩)
4		df-ov 6088	. 2 ⊢ (𝐵𝐹𝐶) = (𝐹‘⟨𝐵, 𝐶⟩)
5	2, 3, 4	3eqtr4g 2296	1 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))

This proof depends on syntax axioms:   → wi 4   = wceq 1402  ⟨cop 3712  ‘cfv 5377  (class class class)co 6085

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385  df-ov 6088

This theorem is used by:  oveq12  6094  oveq1i  6095  oveq1d  6100  ovrspc2v  6111  oveqrspc2v  6112  rspceov  6128  fovcld  6193  ovmpos  6212  ov2gf  6213  ovi3  6226  caovclg  6242  caovcomg  6245  caovassg  6248  caovcang  6251  caovcan  6254  caovordig  6255  caovordg  6257  caovord  6261  caovdig  6264  caovdirg  6267  caovimo  6283  suppssov1  6299  off  6315  caofid0r  6330  caofid1  6331  caofdig  6336  suppofss1dcl  6504  suppofss2dcl  6505  omcl  6734  oeicl  6735  omv2  6738  nnm0r  6752  nnacom  6757  nndi  6759  nnmass  6760  nnmsucr  6761  nnmcom  6762  nnaword  6784  nnmord  6790  nnm00  6803  eroveu  6900  th3qlem2  6912  th3q  6914  ecovcom  6916  ecovicom  6917  ecovass  6918  ecoviass  6919  ecovdi  6920  ecovidi  6921  map0g  6969  addcmpblnq  7734  addclnq  7742  mulclnq  7743  mulidnq  7756  recexnq  7757  recmulnqg  7758  ltanqg  7767  ltmnqg  7768  ltexnqq  7775  enq0ref  7800  enq0tr  7801  addcmpblnq0  7810  mulnnnq0  7817  addclnq0  7818  mulclnq0  7819  distrnq0  7826  mulcomnq0  7827  addassnq0  7829  prarloclemlo  7861  prarloclem3  7864  prarloclem5  7867  prarloclemcalc  7869  genipv  7876  genpassl  7891  genpassu  7892  addlocprlemeq  7900  distrlem4prl  7951  distrlem4pru  7952  ltexprlemdisj  7973  ltexprlemloc  7974  ltexprlemrl  7977  ltexprlemru  7979  prplnqu  7987  cauappcvgprlemm  8012  cauappcvgprlemopl  8013  cauappcvgprlemlol  8014  cauappcvgprlemdisj  8018  cauappcvgprlemloc  8019  cauappcvgprlemladdfl  8022  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  cauappcvgprlem1  8026  cauappcvgprlemlim  8028  cauappcvgpr  8029  caucvgprlemm  8035  caucvgprlemopl  8036  caucvgprlemlol  8037  caucvgprlemdisj  8041  caucvgprlemloc  8042  caucvgprlemladdrl  8045  caucvgprlem1  8046  caucvgpr  8049  caucvgprprlemell  8052  caucvgprprlemml  8061  caucvgprpr  8079  mulcmpblnrlemg  8107  addclsr  8120  mulclsr  8121  0idsr  8134  1idsr  8135  00sr  8136  ltasrg  8137  recexgt0sr  8140  mulgt0sr  8145  mulextsr1  8148  prsrriota  8155  caucvgsrlemgt1  8162  caucvgsrlemoffres  8167  pitonn  8215  peano2nnnn  8220  axaddrcl  8232  axmulrcl  8234  axaddcom  8237  ax1rid  8244  ax0id  8245  axprecex  8247  axcnre  8248  axpre-ltadd  8253  axpre-mulgt0  8254  axpre-mulext  8255  rereceu  8256  peano5nnnn  8259  axcaucvglemcau  8265  axcaucvglemres  8266  mulrid  8323  cnegexlem1  8501  cnegexlem2  8502  cnegex  8504  addcan2  8507  subval  8518  addlsub  8696  apreim  8931  recexap  8981  receuap  8999  divvalap  9004  cju  9291  peano2nn  9316  nn1m1nn  9322  nn1suc  9323  nnsub  9343  fv0p1e1  9419  nnm1nn0  9604  zdiv  9734  zneo  9747  nneoor  9748  zeo  9751  peano5uzti  9754  nn0ind-raph  9763  uzind4s  9990  uzind4s2  9991  qmulz  10023  elpq  10049  cnref1o  10051  nn0ledivnn  10168  xaddnemnf  10259  xaddnepnf  10260  xaddcom  10263  xaddid1  10264  xnn0xadd0  10269  xaddass  10271  xpncan  10273  xleadd1a  10275  xltadd1  10278  xlt2add  10282  xsubge0  10283  xposdif  10284  xlesubadd  10285  xleaddadd  10289  fzsuc2  10486  fzm1  10507  fzoval  10555  exbtwnzlemstep  10682  exbtwnzlemshrink  10683  exbtwnzlemex  10684  exbtwnz  10685  rebtwn2zlemstep  10687  rebtwn2zlemshrink  10688  rebtwn2z  10689  flqlelt  10711  flqbi  10725  fldiv4p1lem1div2  10740  fldiv4lem1div2  10742  modqval  10761  modqadd1  10798  modqmuladd  10803  modqmuladdnn0  10805  modqm1p1mod0  10812  modqmul1  10814  modfzo0difsn  10832  addmodlteq  10835  frec2uzzd  10837  frec2uzsucd  10838  frec2uzrand  10842  frecuzrdgrrn  10845  frec2uzrdg  10846  frecuzrdgrcl  10847  frecuzrdgsuc  10851  frecuzrdgrclt  10852  frecuzrdgg  10853  frecuzrdgdom  10855  frecuzrdgfun  10857  frecuzrdgsuctlem  10860  frecuzrdgsuct  10861  uzsinds  10881  iseqvalcbv  10896  seq3val  10897  seqvalcd  10898  seqf  10901  seq3p1  10902  seqovcd  10904  seqp1cd  10907  seq3fveq2  10912  seqfveq2g  10914  seq3shft2  10918  seqshft2g  10919  monoord  10922  monoord2  10923  seq3split  10925  seqsplitg  10926  seq3caopr3  10928  seqcaopr3g  10929  seq3caopr2  10930  seqcaopr2g  10931  iseqf1olemqval  10937  iseqf1olemqk  10944  seqf1oglem2a  10955  seqf1oglem2  10957  seq3id2  10963  seq3homo  10964  seq3z  10965  seqhomog  10967  seqfeq4g  10968  seq3distr  10969  m1expcl2  10998  mulexp  11015  expadd  11018  expmul  11021  sq0i  11068  qsqeqor  11087  resq01  11095  sqoddm1div8  11131  facp1  11168  faclbnd  11179  faclbnd3  11181  bcval  11187  bcn1  11196  bcval5  11201  bcpasc  11204  bccl  11205  hashfz1  11222  omgadd  11242  hashfzo  11263  hashfzp1  11265  hashxp  11267  hashmap  11268  hashf1lem2  11286  seq3coll  11294  lsw1  11354  ccats1val2  11408  ccatw2s1p2  11414  pfxsuff1eqwrdeq  11471  swrdswrd  11477  ccats1pfxeq  11486  ccatopth  11488  wrdind  11494  wrd2ind  11495  swrdccatin2  11501  pfxccatin12lem2  11503  swrdccat3blem  11511  ccats1pfxeqbi  11514  swrdccatin2d  11516  reuccatpfxs1  11519  shftlem  11581  shftfvalg  11583  shftfibg  11585  shftfval  11586  shftfib  11588  shftfn  11589  shftf  11595  2shfti  11596  shftvalg  11601  shftval4g  11602  cjval  11610  imval  11615  cjexp  11658  sq01  11660  cnrecnv  11676  cvg1nlemcau  11750  cvg1nlemres  11751  resqrexlemcalc3  11782  resqrexlemex  11791  rsqrmo  11793  resqrtcl  11795  rersqrtthlem  11796  sqrtsq  11810  absexp  11845  recan  11875  climshft  12070  climcn1  12074  climcn2  12075  subcn2  12077  fsumshft  12211  fisum0diag2  12214  fsumiun  12244  binomlem  12250  binom  12251  bcxmas  12256  isumsplit  12258  arisum2  12266  trireciplem  12267  trirecip  12268  geolim  12278  cvgratnnlemnexp  12291  cvgratnnlemmn  12292  clim2prod  12306  prodfrecap  12313  fprodcl2lem  12372  fprodfac  12382  fprodshft  12385  ef0lem  12427  efval  12428  efne0  12445  efexp  12449  demoivreALT  12541  dvdsval2  12557  p1modz1  12561  dvds0lem  12568  dvds1lem  12569  dvds2lem  12570  dvdsmulc  12586  divconjdvds  12616  odd2np1lem  12639  odd2np1  12640  ltoddhalfle  12660  halfleoddlt  12661  nn0o1gt2  12672  nn0o  12674  divalglemnn  12685  divalglemeunn  12688  divalglemex  12689  divalglemeuneg  12690  flodddiv4  12703  bitsinv1  12729  gcdabs1  12766  gcddiv  12796  dvdssqim  12801  rpmulgcd  12803  bezoutr1  12810  uzwodc  12814  dvdslcm  12847  lcmeq0  12849  lcmdvds  12857  divgcdcoprm0  12879  prmind2  12898  isprm5lem  12919  isprm6  12925  rpexp  12931  sqrt2irr  12940  pw2dvdslemn  12943  pw2dvdseu  12946  oddpwdclemxy  12947  nn0gcdsq  12978  phicl2  12992  phibndlem  12994  hashdvds  12999  crth  13002  phimullem  13003  eulerthlem1  13005  eulerthlemfi  13006  eulerthlemrprm  13007  eulerthlemth  13010  eulerth  13011  hashgcdlem  13016  phisum  13019  odzval  13020  modprm0  13033  nnnn0modprm0  13034  pythagtriplem1  13044  pythagtriplem6  13049  pythagtriplem7  13050  pythagtriplem12  13054  pythagtriplem14  13056  pythagtriplem18  13060  pythagtriplem19  13061  pceulem  13073  pceu  13074  pcval  13075  pczpre  13076  pcdiv  13081  pcqmul  13082  pcqcl  13085  pcexp  13088  pcaddlem  13118  pcadd  13119  pcmpt  13122  pcprod  13125  pcfac  13129  expnprm  13132  prmpwdvds  13134  pockthi  13137  1arithlem2  13143  4sqlem2  13168  4sqlem3  13169  4sqlem11  13180  4sqlem12  13181  4sqlem13m  13182  4sqlem17  13186  4sqlem18  13187  4sqlem19  13188  ballotfilemfc0  13232  ballotfilemfcc  13233  ennnfonelemr  13314  ctinfom  13319  infpn2  13347  ercpbl  13652  mgm1  13690  mgmidmo  13692  ismgmid  13697  mgmlrid  13699  ismgmid2  13700  lidrideqd  13701  lidrididd  13702  mgmidsssn0  13704  grprida  13707  gzsumfzval  13711  gzsumress  13712  gzsumval2  13714  isnsgrp  13721  sgrpass  13723  sgrp1  13726  sgrpidmndm  13733  ismndd  13750  mndinvmod  13758  imasmnd2  13759  mnd1  13762  mnd1id  13763  mhmpropd  13773  insubm  13792  mhmima  13798  gsumvallem2  13800  grppropd  13822  isgrpd2  13826  isgrpd  13828  dfgrp2  13832  grprcan  13842  grpinveu  13843  grpsubval  13851  grplinv  13855  grpinvid2  13858  isgrpinv  13859  grplrinv  13862  grpidinv2  13863  grpidinv  13864  grpidssd  13881  grpinvssd  13882  dfgrp3mlem  13903  dfgrp3m  13904  grplactfval  13906  grp1  13911  imasgrp2  13913  mhmmnd  13919  ghmgrp  13921  mulgnn0gzsum  13931  mulgnn0p1  13936  mulgnn0subcl  13938  mulgaddcom  13949  mulginvcom  13950  mulgnn0z  13952  mulgneg2  13959  mulgnnass  13960  mulgnn0ass  13961  mhmmulg  13966  issubg  13976  subgex  13979  issubg2m  13992  issubg4m  13996  isnsg2  14006  nsgbi  14007  isnsg3  14010  elnmz  14011  nmzbi  14012  ghmrn  14060  ghmnsgima  14071  gzsumconst  14143  gzsumshift  14149  gsumvalfi  14152  rngdi  14239  rngdir  14240  srgrz  14288  srgmulgass  14293  srgpcomp  14294  srgrmhm  14298  ringid  14331  ringinvnzdiv  14355  mulgass2  14363  ring1  14364  ringrghm  14367  imasring  14369  dvdsrmuld  14403  dvdsrmul1  14409  dvdsr01  14411  dvreq1  14449  rhmdvdsr  14482  lringuplu  14503  issubrng  14507  issubrng2  14518  issubrg  14529  issubrg2  14549  isrrg  14571  domneq0  14581  lmodlema  14628  islmodd  14629  lmodvsmmulgdi  14660  rmodislmodlem  14687  rmodislmod  14688  lssclg  14701  lss1d  14720  lspsn  14753  sraval  14774  rnglidlmcl  14817  quscrng  14870  cnfldmulg  14913  cnfldexp  14914  gsumfsum  14923  cnfldui  14924  expghmap  14942  mulgghm2  14943  mulgrhm  14944  zrhmulg  14955  zlmval  14962  znunit  14994  assalem  15003  asclvald  15022  assamulgscmlem2  15042  assamulgscm  15043  cnmptcom  15399  psmettri2  15429  isxmet2d  15449  xmeteq0  15460  xmettri2  15462  metrest  15607  mpomulcn  15667  expcn  15670  cncfval  15673  mulc1cncf  15690  addccncf  15701  mulcncf  15709  expcncf  15710  hovera  15748  hoverb  15749  hoverlt1  15750  hovergt0  15751  ivthdich  15754  limccnp2lem  15777  dvcnp2cntop  15800  dvcoapbr  15808  dvexp  15812  dvrecap  15814  dvef  15828  plyadd  15852  plymul  15853  plycoeid3  15858  plyco  15860  plycjlemc  15861  plycj  15862  plyrecj  15864  dvply1  15866  dvply2g  15867  sincn  15870  coscn  15871  ptolemy  15925  sincosq1eq  15940  rpcxpmul2  16015  logbgcd1irr  16069  logbgcd1irraplemexp  16070  2irrexpq  16078  2irrexpqap  16080  pellexlem3  16093  mpodvdsmulf1o  16104  fsumdvdsmul  16105  sgmppw  16106  sgmmul  16110  perfect  16115  lgslem4  16122  lgsval  16123  lgsfvalg  16124  lgsval2lem  16129  lgsdir2lem4  16150  lgsdir  16154  lgsdilem2  16155  lgsdi  16156  lgsne0  16157  lgsmodeq  16164  lgsdirnn0  16166  lgsdinn0  16167  gausslemma2dlem0i  16176  gausslemma2dlem1a  16177  gausslemma2dlem1f1o  16179  gausslemma2dlem2  16181  gausslemma2dlem3  16182  gausslemma2dlem4  16183  lgseisenlem2  16190  lgsquadlem2  16197  lgsquadlem3  16198  lgsquad  16199  lgsquad2lem2  16201  2lgslem1a  16207  2lgslem1b  16208  2lgslem1c  16209  2lgslem3a  16212  2lgslem3b  16213  2lgslem3c  16214  2lgslem3d  16215  2lgslem3a1  16216  2lgslem3b1  16217  2lgslem3c1  16218  2lgslem3d1  16219  2lgs  16223  2lgsoddprmlem1  16224  2lgsoddprmlem3  16230  2sqlem2  16234  2sqlem6  16239  2sqlem8  16242  2sqlem9  16243  wlklenvm1  16582  wlklenvm1g  16583  wlkl1loop  16599  2wlklem  16617  clwwlknnn  16653  clwwlknp  16658  clwwlkn1  16659  clwwlkn2  16662  clwwlkext2edg  16663  umgr2cwwk2dif  16665  clwwlknon  16670  clwwlk0on0  16672  clwwlknonex2lem1  16678  clwwlknonex2lem2  16679  clwwlknonex2  16680  qdencn  17072  isomninn  17080  trirec0  17093  iswomninn  17100  ismkvnn  17103