Theorem oveq1 5951

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 3819	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
2	1	fveq2d 5580	. 2 ⊢ (𝐴 = 𝐵 → (𝐹‘⟨𝐴, 𝐶⟩) = (𝐹‘⟨𝐵, 𝐶⟩))
3		df-ov 5947	. 2 ⊢ (𝐴𝐹𝐶) = (𝐹‘⟨𝐴, 𝐶⟩)
4		df-ov 5947	. 2 ⊢ (𝐵𝐹𝐶) = (𝐹‘⟨𝐵, 𝐶⟩)
5	2, 3, 4	3eqtr4g 2263	1 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))

Syntax hints:   → wi 4   = wceq 1373  ⟨cop 3636  ‘cfv 5271  (class class class)co 5944

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 4045  df-iota 5232  df-fv 5279  df-ov 5947

This theorem is referenced by:  oveq12  5953  oveq1i  5954  oveq1d  5959  ovrspc2v  5970  oveqrspc2v  5971  rspceov  5987  fovcld  6050  ovmpos  6069  ov2gf  6070  ovi3  6083  caovclg  6099  caovcomg  6102  caovassg  6105  caovcang  6108  caovcan  6111  caovordig  6112  caovordg  6114  caovord  6118  caovdig  6121  caovdirg  6124  caovimo  6140  suppssov1  6155  off  6171  caofid0r  6186  caofid1  6187  caofdig  6192  omcl  6547  oeicl  6548  omv2  6551  nnm0r  6565  nnacom  6570  nndi  6572  nnmass  6573  nnmsucr  6574  nnmcom  6575  nnaword  6597  nnmord  6603  nnm00  6616  eroveu  6713  th3qlem2  6725  th3q  6727  ecovcom  6729  ecovicom  6730  ecovass  6731  ecoviass  6732  ecovdi  6733  ecovidi  6734  map0g  6775  addcmpblnq  7480  addclnq  7488  mulclnq  7489  mulidnq  7502  recexnq  7503  recmulnqg  7504  ltanqg  7513  ltmnqg  7514  ltexnqq  7521  enq0ref  7546  enq0tr  7547  addcmpblnq0  7556  mulnnnq0  7563  addclnq0  7564  mulclnq0  7565  distrnq0  7572  mulcomnq0  7573  addassnq0  7575  prarloclemlo  7607  prarloclem3  7610  prarloclem5  7613  prarloclemcalc  7615  genipv  7622  genpassl  7637  genpassu  7638  addlocprlemeq  7646  distrlem4prl  7697  distrlem4pru  7698  ltexprlemdisj  7719  ltexprlemloc  7720  ltexprlemrl  7723  ltexprlemru  7725  prplnqu  7733  cauappcvgprlemm  7758  cauappcvgprlemopl  7759  cauappcvgprlemlol  7760  cauappcvgprlemdisj  7764  cauappcvgprlemloc  7765  cauappcvgprlemladdfl  7768  cauappcvgprlemladdru  7769  cauappcvgprlemladdrl  7770  cauappcvgprlem1  7772  cauappcvgprlemlim  7774  cauappcvgpr  7775  caucvgprlemm  7781  caucvgprlemopl  7782  caucvgprlemlol  7783  caucvgprlemdisj  7787  caucvgprlemloc  7788  caucvgprlemladdrl  7791  caucvgprlem1  7792  caucvgpr  7795  caucvgprprlemell  7798  caucvgprprlemml  7807  caucvgprpr  7825  mulcmpblnrlemg  7853  addclsr  7866  mulclsr  7867  0idsr  7880  1idsr  7881  00sr  7882  ltasrg  7883  recexgt0sr  7886  mulgt0sr  7891  mulextsr1  7894  prsrriota  7901  caucvgsrlemgt1  7908  caucvgsrlemoffres  7913  pitonn  7961  peano2nnnn  7966  axaddrcl  7978  axmulrcl  7980  axaddcom  7983  ax1rid  7990  ax0id  7991  axprecex  7993  axcnre  7994  axpre-ltadd  7999  axpre-mulgt0  8000  axpre-mulext  8001  rereceu  8002  peano5nnnn  8005  axcaucvglemcau  8011  axcaucvglemres  8012  mulrid  8069  cnegexlem1  8247  cnegexlem2  8248  cnegex  8250  addcan2  8253  subval  8264  addlsub  8442  apreim  8676  recexap  8726  receuap  8742  divvalap  8747  cju  9034  peano2nn  9048  nn1m1nn  9054  nn1suc  9055  nnsub  9075  fv0p1e1  9151  nnm1nn0  9336  zdiv  9461  zneo  9474  nneoor  9475  zeo  9478  peano5uzti  9481  nn0ind-raph  9490  uzind4s  9711  uzind4s2  9712  qmulz  9744  elpq  9770  cnref1o  9772  nn0ledivnn  9889  xaddnemnf  9979  xaddnepnf  9980  xaddcom  9983  xaddid1  9984  xnn0xadd0  9989  xaddass  9991  xpncan  9993  xleadd1a  9995  xltadd1  9998  xlt2add  10002  xsubge0  10003  xposdif  10004  xlesubadd  10005  xleaddadd  10009  fzsuc2  10201  fzm1  10222  fzoval  10270  exbtwnzlemstep  10390  exbtwnzlemshrink  10391  exbtwnzlemex  10392  exbtwnz  10393  rebtwn2zlemstep  10395  rebtwn2zlemshrink  10396  rebtwn2z  10397  flqlelt  10419  flqbi  10433  fldiv4p1lem1div2  10448  fldiv4lem1div2  10450  modqval  10469  modqadd1  10506  modqmuladd  10511  modqmuladdnn0  10513  modqm1p1mod0  10520  modqmul1  10522  modfzo0difsn  10540  addmodlteq  10543  frec2uzzd  10545  frec2uzsucd  10546  frec2uzrand  10550  frecuzrdgrrn  10553  frec2uzrdg  10554  frecuzrdgrcl  10555  frecuzrdgsuc  10559  frecuzrdgrclt  10560  frecuzrdgg  10561  frecuzrdgdom  10563  frecuzrdgfun  10565  frecuzrdgsuctlem  10568  frecuzrdgsuct  10569  uzsinds  10589  iseqvalcbv  10604  seq3val  10605  seqvalcd  10606  seqf  10609  seq3p1  10610  seqovcd  10612  seqp1cd  10615  seq3fveq2  10620  seqfveq2g  10622  seq3shft2  10626  seqshft2g  10627  monoord  10630  monoord2  10631  seq3split  10633  seqsplitg  10634  seq3caopr3  10636  seqcaopr3g  10637  seq3caopr2  10638  seqcaopr2g  10639  iseqf1olemqval  10645  iseqf1olemqk  10652  seqf1oglem2a  10663  seqf1oglem2  10665  seq3id2  10671  seq3homo  10672  seq3z  10673  seqhomog  10675  seqfeq4g  10676  seq3distr  10677  m1expcl2  10706  mulexp  10723  expadd  10726  expmul  10729  sq0i  10776  qsqeqor  10795  sqoddm1div8  10838  facp1  10875  faclbnd  10886  faclbnd3  10888  bcval  10894  bcn1  10903  bcval5  10908  bcpasc  10911  bccl  10912  hashfz1  10928  omgadd  10947  hashfzo  10967  hashfzp1  10969  hashxp  10971  seq3coll  10987  lsw1  11043  ccats1val2  11092  ccatw2s1p2  11097  shftlem  11127  shftfvalg  11129  shftfibg  11131  shftfval  11132  shftfib  11134  shftfn  11135  shftf  11141  2shfti  11142  shftvalg  11147  shftval4g  11148  cjval  11156  imval  11161  cjexp  11204  cnrecnv  11221  cvg1nlemcau  11295  cvg1nlemres  11296  resqrexlemcalc3  11327  resqrexlemex  11336  rsqrmo  11338  resqrtcl  11340  rersqrtthlem  11341  sqrtsq  11355  absexp  11390  recan  11420  climshft  11615  climcn1  11619  climcn2  11620  subcn2  11622  fsumshft  11755  fisum0diag2  11758  fsumiun  11788  binomlem  11794  binom  11795  bcxmas  11800  isumsplit  11802  arisum2  11810  trireciplem  11811  trirecip  11812  geolim  11822  cvgratnnlemnexp  11835  cvgratnnlemmn  11836  clim2prod  11850  prodfrecap  11857  fprodcl2lem  11916  fprodfac  11926  fprodshft  11929  ef0lem  11971  efval  11972  efne0  11989  efexp  11993  demoivreALT  12085  dvdsval2  12101  p1modz1  12105  dvds0lem  12112  dvds1lem  12113  dvds2lem  12114  dvdsmulc  12130  divconjdvds  12160  odd2np1lem  12183  odd2np1  12184  ltoddhalfle  12204  halfleoddlt  12205  nn0o1gt2  12216  nn0o  12218  divalglemnn  12229  divalglemeunn  12232  divalglemex  12233  divalglemeuneg  12234  flodddiv4  12247  bitsinv1  12273  gcdabs1  12310  gcddiv  12340  dvdssqim  12345  rpmulgcd  12347  bezoutr1  12354  uzwodc  12358  dvdslcm  12391  lcmeq0  12393  lcmdvds  12401  divgcdcoprm0  12423  prmind2  12442  isprm5lem  12463  isprm6  12469  rpexp  12475  sqrt2irr  12484  pw2dvdslemn  12487  pw2dvdseu  12490  oddpwdclemxy  12491  nn0gcdsq  12522  phicl2  12536  phibndlem  12538  hashdvds  12543  crth  12546  phimullem  12547  eulerthlem1  12549  eulerthlemfi  12550  eulerthlemrprm  12551  eulerthlemth  12554  eulerth  12555  hashgcdlem  12560  phisum  12563  odzval  12564  modprm0  12577  nnnn0modprm0  12578  pythagtriplem1  12588  pythagtriplem6  12593  pythagtriplem7  12594  pythagtriplem12  12598  pythagtriplem14  12600  pythagtriplem18  12604  pythagtriplem19  12605  pceulem  12617  pceu  12618  pcval  12619  pczpre  12620  pcdiv  12625  pcqmul  12626  pcqcl  12629  pcexp  12632  pcaddlem  12662  pcadd  12663  pcmpt  12666  pcprod  12669  pcfac  12673  expnprm  12676  prmpwdvds  12678  pockthi  12681  1arithlem2  12687  4sqlem2  12712  4sqlem3  12713  4sqlem11  12724  4sqlem12  12725  4sqlem13m  12726  4sqlem17  12730  4sqlem18  12731  4sqlem19  12732  ennnfonelemr  12794  ctinfom  12799  infpn2  12827  ercpbl  13163  mgm1  13202  mgmidmo  13204  ismgmid  13209  mgmlrid  13211  ismgmid2  13212  lidrideqd  13213  lidrididd  13214  mgmidsssn0  13216  grprida  13219  gsumfzval  13223  gsumress  13227  gsumval2  13229  isnsgrp  13238  sgrpass  13240  sgrp1  13243  sgrpidmndm  13252  ismndd  13269  mndinvmod  13277  imasmnd2  13284  mnd1  13287  mnd1id  13288  mhmpropd  13298  insubm  13317  mhmima  13323  gsumvallem2  13325  grppropd  13349  isgrpd2  13353  isgrpd  13355  dfgrp2  13359  grprcan  13369  grpinveu  13370  grpsubval  13378  grplinv  13382  grpinvid2  13385  isgrpinv  13386  grplrinv  13389  grpidinv2  13390  grpidinv  13391  grpidssd  13408  grpinvssd  13409  dfgrp3mlem  13430  dfgrp3m  13431  grplactfval  13433  grp1  13438  imasgrp2  13446  mhmmnd  13452  ghmgrp  13454  mulgnn0gsum  13464  mulgnn0p1  13469  mulgnn0subcl  13471  mulgaddcom  13482  mulginvcom  13483  mulgnn0z  13485  mulgneg2  13492  mulgnnass  13493  mulgnn0ass  13494  mhmmulg  13499  issubg  13509  subgex  13512  issubg2m  13525  issubg4m  13529  isnsg2  13539  nsgbi  13540  isnsg3  13543  elnmz  13544  nmzbi  13545  ghmrn  13593  ghmnsgima  13604  gsumfzconst  13677  rngdi  13702  rngdir  13703  srgrz  13746  srgmulgass  13751  srgpcomp  13752  srgrmhm  13756  ringid  13788  ringinvnzdiv  13812  mulgass2  13820  ring1  13821  ringrghm  13824  imasring  13826  dvdsrmuld  13858  dvdsrmul1  13864  dvdsr01  13866  dvreq1  13904  rhmdvdsr  13937  lringuplu  13958  issubrng  13961  issubrng2  13972  issubrg  13983  issubrg2  14003  isrrg  14025  domneq0  14034  lmodlema  14054  islmodd  14055  lmodvsmmulgdi  14085  rmodislmodlem  14112  rmodislmod  14113  lssclg  14126  lss1d  14145  lspsn  14178  sraval  14199  rnglidlmcl  14242  quscrng  14295  cnfldmulg  14338  cnfldexp  14339  gsumfzfsumlemm  14349  cnfldui  14351  expghmap  14369  mulgghm2  14370  mulgrhm  14371  zrhmulg  14382  zlmval  14389  znunit  14421  cnmptcom  14770  psmettri2  14800  isxmet2d  14820  xmeteq0  14831  xmettri2  14833  metrest  14978  mpomulcn  15038  expcn  15041  cncfval  15044  mulc1cncf  15061  addccncf  15072  mulcncf  15080  expcncf  15081  hovera  15119  hoverb  15120  hoverlt1  15121  hovergt0  15122  ivthdich  15125  limccnp2lem  15148  dvcnp2cntop  15171  dvcoapbr  15179  dvexp  15183  dvrecap  15185  dvef  15199  plyadd  15223  plymul  15224  plycoeid3  15229  plyco  15231  plycjlemc  15232  plycj  15233  plyrecj  15235  dvply1  15237  dvply2g  15238  sincn  15241  coscn  15242  ptolemy  15296  sincosq1eq  15311  rpcxpmul2  15385  logbgcd1irr  15439  logbgcd1irraplemexp  15440  2irrexpq  15448  2irrexpqap  15450  mpodvdsmulf1o  15462  fsumdvdsmul  15463  sgmppw  15464  sgmmul  15468  perfect  15473  lgslem4  15480  lgsval  15481  lgsfvalg  15482  lgsval2lem  15487  lgsdir2lem4  15508  lgsdir  15512  lgsdilem2  15513  lgsdi  15514  lgsne0  15515  lgsmodeq  15522  lgsdirnn0  15524  lgsdinn0  15525  gausslemma2dlem0i  15534  gausslemma2dlem1a  15535  gausslemma2dlem1f1o  15537  gausslemma2dlem2  15539  gausslemma2dlem3  15540  gausslemma2dlem4  15541  lgseisenlem2  15548  lgsquadlem2  15555  lgsquadlem3  15556  lgsquad  15557  lgsquad2lem2  15559  2lgslem1a  15565  2lgslem1b  15566  2lgslem1c  15567  2lgslem3a  15570  2lgslem3b  15571  2lgslem3c  15572  2lgslem3d  15573  2lgslem3a1  15574  2lgslem3b1  15575  2lgslem3c1  15576  2lgslem3d1  15577  2lgs  15581  2lgsoddprmlem1  15582  2lgsoddprmlem3  15588  2sqlem2  15592  2sqlem6  15597  2sqlem8  15600  2sqlem9  15601  qdencn  15966  isomninn  15970  trirec0  15983  iswomninn  15989  ismkvnn  15992