Theorem oveq1 5697

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 3644	. . 3 |- ( A = B -> <. A , C >. = <. B , C >. )
2	1	fveq2d 5344	. 2 |- ( A = B -> ( F ` <. A , C >. ) = ( F ` <. B , C >. ) )
3		df-ov 5693	. 2 |- ( A F C ) = ( F ` <. A , C >. )
4		df-ov 5693	. 2 |- ( B F C ) = ( F ` <. B , C >. )
5	2, 3, 4	3eqtr4g 2152	1 |- ( A = B -> ( A F C ) = ( B F C ) )

Syntax hints:   -> wi 4   = wceq 1296   <.cop 3469   ` cfv 5049  (class class class)co 5690

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-3an 929  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-rex 2376  df-v 2635  df-un 3017  df-sn 3472  df-pr 3473  df-op 3475  df-uni 3676  df-br 3868  df-iota 5014  df-fv 5057  df-ov 5693

This theorem is referenced by:  oveq12  5699  oveq1i  5700  oveq1d  5705  rspceov  5729  fovcl  5788  ovmpt2s  5806  ov2gf  5807  ovi3  5819  caovclg  5835  caovcomg  5838  caovassg  5841  caovcang  5844  caovcan  5847  caovordig  5848  caovordg  5850  caovord  5854  caovdig  5857  caovdirg  5860  caovimo  5876  grpridd  5879  suppssov1  5891  off  5906  omcl  6262  oeicl  6263  omv2  6266  nnm0r  6280  nnacom  6285  nndi  6287  nnmass  6288  nnmsucr  6289  nnmcom  6290  nnaword  6310  nnmord  6316  nnm00  6328  eroveu  6423  th3qlem2  6435  th3q  6437  ecovcom  6439  ecovicom  6440  ecovass  6441  ecoviass  6442  ecovdi  6443  ecovidi  6444  map0g  6485  addcmpblnq  7023  addclnq  7031  mulclnq  7032  mulidnq  7045  recexnq  7046  recmulnqg  7047  ltanqg  7056  ltmnqg  7057  ltexnqq  7064  enq0ref  7089  enq0tr  7090  addcmpblnq0  7099  mulnnnq0  7106  addclnq0  7107  mulclnq0  7108  distrnq0  7115  mulcomnq0  7116  addassnq0  7118  prarloclemlo  7150  prarloclem3  7153  prarloclem5  7156  prarloclemcalc  7158  genipv  7165  genpassl  7180  genpassu  7181  addlocprlemeq  7189  distrlem4prl  7240  distrlem4pru  7241  ltexprlemdisj  7262  ltexprlemloc  7263  ltexprlemrl  7266  ltexprlemru  7268  prplnqu  7276  cauappcvgprlemm  7301  cauappcvgprlemopl  7302  cauappcvgprlemlol  7303  cauappcvgprlemdisj  7307  cauappcvgprlemloc  7308  cauappcvgprlemladdfl  7311  cauappcvgprlemladdru  7312  cauappcvgprlemladdrl  7313  cauappcvgprlem1  7315  cauappcvgprlemlim  7317  cauappcvgpr  7318  caucvgprlemm  7324  caucvgprlemopl  7325  caucvgprlemlol  7326  caucvgprlemdisj  7330  caucvgprlemloc  7331  caucvgprlemladdrl  7334  caucvgprlem1  7335  caucvgpr  7338  caucvgprprlemell  7341  caucvgprprlemml  7350  caucvgprpr  7368  mulcmpblnrlemg  7383  addclsr  7396  mulclsr  7397  0idsr  7410  1idsr  7411  00sr  7412  ltasrg  7413  recexgt0sr  7416  mulgt0sr  7420  mulextsr1  7423  prsrriota  7430  caucvgsrlemgt1  7437  caucvgsrlemoffres  7442  pitonn  7482  peano2nnnn  7487  axaddrcl  7499  axmulrcl  7501  axaddcom  7502  ax1rid  7509  ax0id  7510  axprecex  7512  axcnre  7513  axpre-ltadd  7518  axpre-mulgt0  7519  axpre-mulext  7520  rereceu  7521  peano5nnnn  7524  axcaucvglemcau  7530  axcaucvglemres  7531  mulid1  7582  cnegexlem1  7754  cnegexlem2  7755  cnegex  7757  addcan2  7760  subval  7771  addlsub  7945  apreim  8177  recexap  8219  receuap  8235  divvalap  8238  cju  8519  peano2nn  8532  nn1m1nn  8538  nn1suc  8539  nnsub  8559  fv0p1e1  8635  nnm1nn0  8812  zdiv  8933  zneo  8946  nneoor  8947  zeo  8950  peano5uzti  8953  nn0ind-raph  8962  uzind4s  9177  uzind4s2  9178  qmulz  9207  cnref1o  9232  nn0ledivnn  9337  xaddnemnf  9423  xaddnepnf  9424  xaddcom  9427  xaddid1  9428  xnn0xadd0  9433  xaddass  9435  xpncan  9437  xleadd1a  9439  xltadd1  9442  xlt2add  9446  xsubge0  9447  xposdif  9448  xlesubadd  9449  xleaddadd  9453  fzsuc2  9642  fzm1  9663  fzoval  9708  exbtwnzlemstep  9808  exbtwnzlemshrink  9809  exbtwnzlemex  9810  exbtwnz  9811  rebtwn2zlemstep  9813  rebtwn2zlemshrink  9814  rebtwn2z  9815  flqlelt  9832  flqbi  9846  fldiv4p1lem1div2  9861  modqval  9880  modqadd1  9917  modqmuladd  9922  modqmuladdnn0  9924  modqm1p1mod0  9931  modqmul1  9933  modfzo0difsn  9951  addmodlteq  9954  frec2uzzd  9956  frec2uzsucd  9957  frec2uzrand  9961  frecuzrdgrrn  9964  frec2uzrdg  9965  frecuzrdgrcl  9966  frecuzrdgsuc  9970  frecuzrdgrclt  9971  frecuzrdgg  9972  frecuzrdgdom  9974  frecuzrdgfun  9976  frecuzrdgsuctlem  9979  frecuzrdgsuct  9980  uzsinds  9997  iseqval  10017  iseqvalcbv  10018  iseqvalt  10019  seq3val  10020  iseqfclt  10025  seqf  10026  iseqp1  10028  iseqp1t  10029  seq3p1  10030  iseqsst  10031  seq3fveq2  10034  seq3shft2  10038  monoord  10042  monoord2  10043  seq3split  10045  seq3caopr3  10047  seq3caopr2  10048  iseqf1olemqval  10053  iseqf1olemqk  10060  seq3id2  10075  seq3homo  10076  seq3z  10077  seq3distr  10079  m1expcl2  10108  mulexp  10125  expadd  10128  expmul  10131  sq0i  10177  sqoddm1div8  10237  facp1  10269  faclbnd  10280  faclbnd3  10282  bcval  10288  bcn1  10297  bcval5  10302  bcpasc  10305  bccl  10306  hashfz1  10322  omgadd  10341  hashfzo  10361  hashfzp1  10363  hashxp  10365  seq3coll  10378  shftlem  10381  shftfvalg  10383  shftfibg  10385  shftfval  10386  shftfib  10388  shftfn  10389  shftf  10395  2shfti  10396  shftvalg  10401  shftval4g  10402  cjval  10410  imval  10415  cjexp  10458  cnrecnv  10475  cvg1nlemcau  10548  cvg1nlemres  10549  resqrexlemcalc3  10580  resqrexlemex  10589  rsqrmo  10591  resqrtcl  10593  rersqrtthlem  10594  sqrtsq  10608  absexp  10643  recan  10673  climshft  10863  climcn1  10867  climcn2  10868  subcn2  10870  fsumshft  11003  fisum0diag2  11006  fsumiun  11036  binomlem  11042  binom  11043  bcxmas  11048  isumsplit  11050  arisum2  11058  trireciplem  11059  trirecip  11060  geolim  11070  cvgratnnlemnexp  11083  cvgratnnlemmn  11084  ef0lem  11115  efval  11116  efne0  11133  efexp  11137  demoivreALT  11228  dvdsval2  11242  dvds0lem  11249  dvds1lem  11250  dvds2lem  11251  dvdsmulc  11267  divconjdvds  11293  odd2np1lem  11315  odd2np1  11316  ltoddhalfle  11336  halfleoddlt  11337  nn0o1gt2  11348  nn0o  11350  divalglemnn  11361  divalglemeunn  11364  divalglemex  11365  divalglemeuneg  11366  flodddiv4  11377  gcdabs1  11423  gcddiv  11451  dvdssqim  11456  rpmulgcd  11458  bezoutr1  11465  dvdslcm  11494  lcmeq0  11496  lcmdvds  11504  divgcdcoprm0  11526  prmind2  11545  isprm6  11569  rpexp  11575  sqrt2irr  11584  pw2dvdslemn  11586  pw2dvdseu  11589  oddpwdclemxy  11590  nn0gcdsq  11621  phicl2  11633  phibndlem  11635  hashdvds  11640  crth  11643  phimullem  11644  hashgcdlem  11646  psmettri2  12130  isxmet2d  12150  xmeteq0  12161  xmettri2  12163  metrest  12308  cncfval  12341  mulc1cncf  12358  addccncf  12365  mulcncf  12370  expcncf  12371  qdencn  12636