Theorem oveq1 5953

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

Assertion

Ref	Expression
oveq1	|- ( A = B -> ( A F C ) = ( B F C ) )

Proof of Theorem oveq1

Step	Hyp	Ref	Expression
1		opeq1 3819	. . 3 |- ( A = B -> <. A , C >. = <. B , C >. )
2	1	fveq2d 5582	. 2 |- ( A = B -> ( F ` <. A , C >. ) = ( F ` <. B , C >. ) )
3		df-ov 5949	. 2 |- ( A F C ) = ( F ` <. A , C >. )
4		df-ov 5949	. 2 |- ( B F C ) = ( F ` <. B , C >. )
5	2, 3, 4	3eqtr4g 2263	1 |- ( A = B -> ( A F C ) = ( B F C ) )

Syntax hints:   -> wi 4   = wceq 1373   <.cop 3636   ` cfv 5272  (class class class)co 5946

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4046  df-iota 5233  df-fv 5280  df-ov 5949

This theorem is referenced by:  oveq12  5955  oveq1i  5956  oveq1d  5961  ovrspc2v  5972  oveqrspc2v  5973  rspceov  5989  fovcld  6052  ovmpos  6071  ov2gf  6072  ovi3  6085  caovclg  6101  caovcomg  6104  caovassg  6107  caovcang  6110  caovcan  6113  caovordig  6114  caovordg  6116  caovord  6120  caovdig  6123  caovdirg  6126  caovimo  6142  suppssov1  6157  off  6173  caofid0r  6188  caofid1  6189  caofdig  6194  omcl  6549  oeicl  6550  omv2  6553  nnm0r  6567  nnacom  6572  nndi  6574  nnmass  6575  nnmsucr  6576  nnmcom  6577  nnaword  6599  nnmord  6605  nnm00  6618  eroveu  6715  th3qlem2  6727  th3q  6729  ecovcom  6731  ecovicom  6732  ecovass  6733  ecoviass  6734  ecovdi  6735  ecovidi  6736  map0g  6777  addcmpblnq  7482  addclnq  7490  mulclnq  7491  mulidnq  7504  recexnq  7505  recmulnqg  7506  ltanqg  7515  ltmnqg  7516  ltexnqq  7523  enq0ref  7548  enq0tr  7549  addcmpblnq0  7558  mulnnnq0  7565  addclnq0  7566  mulclnq0  7567  distrnq0  7574  mulcomnq0  7575  addassnq0  7577  prarloclemlo  7609  prarloclem3  7612  prarloclem5  7615  prarloclemcalc  7617  genipv  7624  genpassl  7639  genpassu  7640  addlocprlemeq  7648  distrlem4prl  7699  distrlem4pru  7700  ltexprlemdisj  7721  ltexprlemloc  7722  ltexprlemrl  7725  ltexprlemru  7727  prplnqu  7735  cauappcvgprlemm  7760  cauappcvgprlemopl  7761  cauappcvgprlemlol  7762  cauappcvgprlemdisj  7766  cauappcvgprlemloc  7767  cauappcvgprlemladdfl  7770  cauappcvgprlemladdru  7771  cauappcvgprlemladdrl  7772  cauappcvgprlem1  7774  cauappcvgprlemlim  7776  cauappcvgpr  7777  caucvgprlemm  7783  caucvgprlemopl  7784  caucvgprlemlol  7785  caucvgprlemdisj  7789  caucvgprlemloc  7790  caucvgprlemladdrl  7793  caucvgprlem1  7794  caucvgpr  7797  caucvgprprlemell  7800  caucvgprprlemml  7809  caucvgprpr  7827  mulcmpblnrlemg  7855  addclsr  7868  mulclsr  7869  0idsr  7882  1idsr  7883  00sr  7884  ltasrg  7885  recexgt0sr  7888  mulgt0sr  7893  mulextsr1  7896  prsrriota  7903  caucvgsrlemgt1  7910  caucvgsrlemoffres  7915  pitonn  7963  peano2nnnn  7968  axaddrcl  7980  axmulrcl  7982  axaddcom  7985  ax1rid  7992  ax0id  7993  axprecex  7995  axcnre  7996  axpre-ltadd  8001  axpre-mulgt0  8002  axpre-mulext  8003  rereceu  8004  peano5nnnn  8007  axcaucvglemcau  8013  axcaucvglemres  8014  mulrid  8071  cnegexlem1  8249  cnegexlem2  8250  cnegex  8252  addcan2  8255  subval  8266  addlsub  8444  apreim  8678  recexap  8728  receuap  8744  divvalap  8749  cju  9036  peano2nn  9050  nn1m1nn  9056  nn1suc  9057  nnsub  9077  fv0p1e1  9153  nnm1nn0  9338  zdiv  9463  zneo  9476  nneoor  9477  zeo  9480  peano5uzti  9483  nn0ind-raph  9492  uzind4s  9713  uzind4s2  9714  qmulz  9746  elpq  9772  cnref1o  9774  nn0ledivnn  9891  xaddnemnf  9981  xaddnepnf  9982  xaddcom  9985  xaddid1  9986  xnn0xadd0  9991  xaddass  9993  xpncan  9995  xleadd1a  9997  xltadd1  10000  xlt2add  10004  xsubge0  10005  xposdif  10006  xlesubadd  10007  xleaddadd  10011  fzsuc2  10203  fzm1  10224  fzoval  10272  exbtwnzlemstep  10392  exbtwnzlemshrink  10393  exbtwnzlemex  10394  exbtwnz  10395  rebtwn2zlemstep  10397  rebtwn2zlemshrink  10398  rebtwn2z  10399  flqlelt  10421  flqbi  10435  fldiv4p1lem1div2  10450  fldiv4lem1div2  10452  modqval  10471  modqadd1  10508  modqmuladd  10513  modqmuladdnn0  10515  modqm1p1mod0  10522  modqmul1  10524  modfzo0difsn  10542  addmodlteq  10545  frec2uzzd  10547  frec2uzsucd  10548  frec2uzrand  10552  frecuzrdgrrn  10555  frec2uzrdg  10556  frecuzrdgrcl  10557  frecuzrdgsuc  10561  frecuzrdgrclt  10562  frecuzrdgg  10563  frecuzrdgdom  10565  frecuzrdgfun  10567  frecuzrdgsuctlem  10570  frecuzrdgsuct  10571  uzsinds  10591  iseqvalcbv  10606  seq3val  10607  seqvalcd  10608  seqf  10611  seq3p1  10612  seqovcd  10614  seqp1cd  10617  seq3fveq2  10622  seqfveq2g  10624  seq3shft2  10628  seqshft2g  10629  monoord  10632  monoord2  10633  seq3split  10635  seqsplitg  10636  seq3caopr3  10638  seqcaopr3g  10639  seq3caopr2  10640  seqcaopr2g  10641  iseqf1olemqval  10647  iseqf1olemqk  10654  seqf1oglem2a  10665  seqf1oglem2  10667  seq3id2  10673  seq3homo  10674  seq3z  10675  seqhomog  10677  seqfeq4g  10678  seq3distr  10679  m1expcl2  10708  mulexp  10725  expadd  10728  expmul  10731  sq0i  10778  qsqeqor  10797  sqoddm1div8  10840  facp1  10877  faclbnd  10888  faclbnd3  10890  bcval  10896  bcn1  10905  bcval5  10910  bcpasc  10913  bccl  10914  hashfz1  10930  omgadd  10949  hashfzo  10969  hashfzp1  10971  hashxp  10973  seq3coll  10989  lsw1  11045  ccats1val2  11095  ccatw2s1p2  11100  pfxsuff1eqwrdeq  11153  shftlem  11160  shftfvalg  11162  shftfibg  11164  shftfval  11165  shftfib  11167  shftfn  11168  shftf  11174  2shfti  11175  shftvalg  11180  shftval4g  11181  cjval  11189  imval  11194  cjexp  11237  cnrecnv  11254  cvg1nlemcau  11328  cvg1nlemres  11329  resqrexlemcalc3  11360  resqrexlemex  11369  rsqrmo  11371  resqrtcl  11373  rersqrtthlem  11374  sqrtsq  11388  absexp  11423  recan  11453  climshft  11648  climcn1  11652  climcn2  11653  subcn2  11655  fsumshft  11788  fisum0diag2  11791  fsumiun  11821  binomlem  11827  binom  11828  bcxmas  11833  isumsplit  11835  arisum2  11843  trireciplem  11844  trirecip  11845  geolim  11855  cvgratnnlemnexp  11868  cvgratnnlemmn  11869  clim2prod  11883  prodfrecap  11890  fprodcl2lem  11949  fprodfac  11959  fprodshft  11962  ef0lem  12004  efval  12005  efne0  12022  efexp  12026  demoivreALT  12118  dvdsval2  12134  p1modz1  12138  dvds0lem  12145  dvds1lem  12146  dvds2lem  12147  dvdsmulc  12163  divconjdvds  12193  odd2np1lem  12216  odd2np1  12217  ltoddhalfle  12237  halfleoddlt  12238  nn0o1gt2  12249  nn0o  12251  divalglemnn  12262  divalglemeunn  12265  divalglemex  12266  divalglemeuneg  12267  flodddiv4  12280  bitsinv1  12306  gcdabs1  12343  gcddiv  12373  dvdssqim  12378  rpmulgcd  12380  bezoutr1  12387  uzwodc  12391  dvdslcm  12424  lcmeq0  12426  lcmdvds  12434  divgcdcoprm0  12456  prmind2  12475  isprm5lem  12496  isprm6  12502  rpexp  12508  sqrt2irr  12517  pw2dvdslemn  12520  pw2dvdseu  12523  oddpwdclemxy  12524  nn0gcdsq  12555  phicl2  12569  phibndlem  12571  hashdvds  12576  crth  12579  phimullem  12580  eulerthlem1  12582  eulerthlemfi  12583  eulerthlemrprm  12584  eulerthlemth  12587  eulerth  12588  hashgcdlem  12593  phisum  12596  odzval  12597  modprm0  12610  nnnn0modprm0  12611  pythagtriplem1  12621  pythagtriplem6  12626  pythagtriplem7  12627  pythagtriplem12  12631  pythagtriplem14  12633  pythagtriplem18  12637  pythagtriplem19  12638  pceulem  12650  pceu  12651  pcval  12652  pczpre  12653  pcdiv  12658  pcqmul  12659  pcqcl  12662  pcexp  12665  pcaddlem  12695  pcadd  12696  pcmpt  12699  pcprod  12702  pcfac  12706  expnprm  12709  prmpwdvds  12711  pockthi  12714  1arithlem2  12720  4sqlem2  12745  4sqlem3  12746  4sqlem11  12757  4sqlem12  12758  4sqlem13m  12759  4sqlem17  12763  4sqlem18  12764  4sqlem19  12765  ennnfonelemr  12827  ctinfom  12832  infpn2  12860  ercpbl  13196  mgm1  13235  mgmidmo  13237  ismgmid  13242  mgmlrid  13244  ismgmid2  13245  lidrideqd  13246  lidrididd  13247  mgmidsssn0  13249  grprida  13252  gsumfzval  13256  gsumress  13260  gsumval2  13262  isnsgrp  13271  sgrpass  13273  sgrp1  13276  sgrpidmndm  13285  ismndd  13302  mndinvmod  13310  imasmnd2  13317  mnd1  13320  mnd1id  13321  mhmpropd  13331  insubm  13350  mhmima  13356  gsumvallem2  13358  grppropd  13382  isgrpd2  13386  isgrpd  13388  dfgrp2  13392  grprcan  13402  grpinveu  13403  grpsubval  13411  grplinv  13415  grpinvid2  13418  isgrpinv  13419  grplrinv  13422  grpidinv2  13423  grpidinv  13424  grpidssd  13441  grpinvssd  13442  dfgrp3mlem  13463  dfgrp3m  13464  grplactfval  13466  grp1  13471  imasgrp2  13479  mhmmnd  13485  ghmgrp  13487  mulgnn0gsum  13497  mulgnn0p1  13502  mulgnn0subcl  13504  mulgaddcom  13515  mulginvcom  13516  mulgnn0z  13518  mulgneg2  13525  mulgnnass  13526  mulgnn0ass  13527  mhmmulg  13532  issubg  13542  subgex  13545  issubg2m  13558  issubg4m  13562  isnsg2  13572  nsgbi  13573  isnsg3  13576  elnmz  13577  nmzbi  13578  ghmrn  13626  ghmnsgima  13637  gsumfzconst  13710  rngdi  13735  rngdir  13736  srgrz  13779  srgmulgass  13784  srgpcomp  13785  srgrmhm  13789  ringid  13821  ringinvnzdiv  13845  mulgass2  13853  ring1  13854  ringrghm  13857  imasring  13859  dvdsrmuld  13891  dvdsrmul1  13897  dvdsr01  13899  dvreq1  13937  rhmdvdsr  13970  lringuplu  13991  issubrng  13994  issubrng2  14005  issubrg  14016  issubrg2  14036  isrrg  14058  domneq0  14067  lmodlema  14087  islmodd  14088  lmodvsmmulgdi  14118  rmodislmodlem  14145  rmodislmod  14146  lssclg  14159  lss1d  14178  lspsn  14211  sraval  14232  rnglidlmcl  14275  quscrng  14328  cnfldmulg  14371  cnfldexp  14372  gsumfzfsumlemm  14382  cnfldui  14384  expghmap  14402  mulgghm2  14403  mulgrhm  14404  zrhmulg  14415  zlmval  14422  znunit  14454  cnmptcom  14803  psmettri2  14833  isxmet2d  14853  xmeteq0  14864  xmettri2  14866  metrest  15011  mpomulcn  15071  expcn  15074  cncfval  15077  mulc1cncf  15094  addccncf  15105  mulcncf  15113  expcncf  15114  hovera  15152  hoverb  15153  hoverlt1  15154  hovergt0  15155  ivthdich  15158  limccnp2lem  15181  dvcnp2cntop  15204  dvcoapbr  15212  dvexp  15216  dvrecap  15218  dvef  15232  plyadd  15256  plymul  15257  plycoeid3  15262  plyco  15264  plycjlemc  15265  plycj  15266  plyrecj  15268  dvply1  15270  dvply2g  15271  sincn  15274  coscn  15275  ptolemy  15329  sincosq1eq  15344  rpcxpmul2  15418  logbgcd1irr  15472  logbgcd1irraplemexp  15473  2irrexpq  15481  2irrexpqap  15483  mpodvdsmulf1o  15495  fsumdvdsmul  15496  sgmppw  15497  sgmmul  15501  perfect  15506  lgslem4  15513  lgsval  15514  lgsfvalg  15515  lgsval2lem  15520  lgsdir2lem4  15541  lgsdir  15545  lgsdilem2  15546  lgsdi  15547  lgsne0  15548  lgsmodeq  15555  lgsdirnn0  15557  lgsdinn0  15558  gausslemma2dlem0i  15567  gausslemma2dlem1a  15568  gausslemma2dlem1f1o  15570  gausslemma2dlem2  15572  gausslemma2dlem3  15573  gausslemma2dlem4  15574  lgseisenlem2  15581  lgsquadlem2  15588  lgsquadlem3  15589  lgsquad  15590  lgsquad2lem2  15592  2lgslem1a  15598  2lgslem1b  15599  2lgslem1c  15600  2lgslem3a  15603  2lgslem3b  15604  2lgslem3c  15605  2lgslem3d  15606  2lgslem3a1  15607  2lgslem3b1  15608  2lgslem3c1  15609  2lgslem3d1  15610  2lgs  15614  2lgsoddprmlem1  15615  2lgsoddprmlem3  15621  2sqlem2  15625  2sqlem6  15630  2sqlem8  15633  2sqlem9  15634  qdencn  16003  isomninn  16007  trirec0  16020  iswomninn  16026  ismkvnn  16029