Theorem oveq2 5790

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

Assertion

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

Proof of Theorem oveq2

Step	Hyp	Ref	Expression
1		opeq2 3714	. . 3 |- ( A = B -> <. C , A >. = <. C , B >. )
2	1	fveq2d 5433	. 2 |- ( A = B -> ( F ` <. C , A >. ) = ( F ` <. C , B >. ) )
3		df-ov 5785	. 2 |- ( C F A ) = ( F ` <. C , A >. )
4		df-ov 5785	. 2 |- ( C F B ) = ( F ` <. C , B >. )
5	2, 3, 4	3eqtr4g 2198	1 |- ( A = B -> ( C F A ) = ( C F B ) )

Syntax hints:   -> wi 4   = wceq 1332   <.cop 3535   ` cfv 5131  (class class class)co 5782

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 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rex 2423  df-v 2691  df-un 3080  df-sn 3538  df-pr 3539  df-op 3541  df-uni 3745  df-br 3938  df-iota 5096  df-fv 5139  df-ov 5785

This theorem is referenced by:  oveq12  5791  oveq2i  5793  oveq2d  5798  ovanraleqv  5806  rspceov  5821  fovcl  5884  ovmpos  5902  ov2gf  5903  ovi3  5915  caovclg  5931  caovcomg  5934  caovassg  5937  caovcang  5940  caovcan  5943  caovordig  5944  caovordg  5946  caovord  5950  caovdig  5953  caovdirg  5956  caovimo  5972  grprinvlem  5973  grprinvd  5974  suppssov1  5987  off  6002  omv  6359  oeiv  6360  oasuc  6368  oawordriexmid  6374  omsuc  6376  nna0r  6382  nnm0r  6383  nnacl  6384  nnmcl  6385  nnacom  6388  nnaass  6389  nndi  6390  nnmass  6391  nnmsucr  6392  nnmcom  6393  nnaordi  6412  nnaord  6413  nnmordi  6420  nnmord  6421  nnaordex  6431  nnawordex  6432  nnm00  6433  eroveu  6528  ecopovtrn  6534  ecopovtrng  6537  th3qlem2  6540  th3q  6542  ecovcom  6544  ecovicom  6545  ecovass  6546  ecoviass  6547  ecovdi  6548  ecovidi  6549  addcanpig  7166  mulcanpig  7167  addcmpblnq  7199  addclnq  7207  mulclnq  7208  recexnq  7222  recmulnqg  7223  ltanqg  7232  ltmnqg  7233  ltexnqq  7240  enq0ref  7265  enq0tr  7266  addcmpblnq0  7275  mulnnnq0  7282  addclnq0  7283  mulclnq0  7284  distrnq0  7291  mulcomnq0  7292  addassnq0  7294  nq02m  7297  prarloclem3  7329  genipv  7341  genpassl  7356  genpassu  7357  addlocpr  7368  distrlem1prl  7414  distrlem1pru  7415  1idprl  7422  1idpru  7423  ltexprlemell  7430  ltexprlemelu  7431  ltexpri  7445  lteupri  7449  ltaprlem  7450  recexprlem1ssl  7465  recexprlem1ssu  7466  recexpr  7470  cauappcvgprlemm  7477  cauappcvgprlemdisj  7483  cauappcvgprlemloc  7484  cauappcvgprlemladdru  7488  cauappcvgprlemladdrl  7489  cauappcvgprlem1  7491  cauappcvgprlemlim  7493  cauappcvgpr  7494  mulcmpblnrlemg  7572  addclsr  7585  mulclsr  7586  ltasrg  7602  negexsr  7604  recexgt0sr  7605  mulgt0sr  7610  mulextsr1  7613  srpospr  7615  caucvgsrlemgt1  7627  map2psrprg  7637  axaddrcl  7697  axmulrcl  7699  axaddcom  7702  axrnegex  7711  axprecex  7712  axcnre  7713  axpre-ltadd  7718  axpre-mulgt0  7719  axpre-mulext  7720  rereceu  7721  recriota  7722  axcaucvglemres  7731  readdcan  7926  cnegexlem1  7961  cnegex  7964  addcan  7966  negeq  7979  subadd  7989  addid0  8159  ine0  8180  rimul  8371  cru  8388  apreim  8389  recexap  8438  mulcanapd  8446  receuap  8454  divmulap  8459  cju  8743  nnaddcl  8764  nnmulcl  8765  nnsub  8783  nnnn0addcl  9031  zaddcllempos  9115  zaddcl  9118  zdiv  9163  deceq1  9210  deceq2  9211  uzaddcl  9408  zq  9445  qreccl  9461  cnref1o  9469  xaddnemnf  9670  xaddnepnf  9671  xaddcom  9674  xnn0xadd0  9680  xnegdi  9681  xaddass  9682  xlt2add  9693  xlesubadd  9696  xleaddadd  9700  fzsuc2  9890  fzrevral  9916  fzshftral  9919  2ffzeq  9949  exfzdc  10048  exbtwnzlemshrink  10057  rebtwn2zlemshrink  10062  modqval  10128  modqmuladd  10170  modqmuladdnn0  10172  frecuzrdgrrn  10212  frec2uzrdg  10213  frecuzrdgrcl  10214  frecuzrdgsuc  10218  frecuzrdgrclt  10219  frecuzrdgg  10220  frecuzrdgsuctlem  10227  frecfzennn  10230  uzsinds  10246  iseqvalcbv  10261  seq3val  10262  seqvalcd  10263  seqovcd  10267  seq3caopr3  10285  seq3caopr2  10286  seq3f1olemp  10306  seq3id  10312  seq3homo  10314  seq3z  10315  seq3distr  10317  expp1  10331  expnegap0  10332  expcllem  10335  expcl2lemap  10336  m1expcl2  10346  expap0  10354  mulexp  10363  expadd  10366  expmul  10369  leexp2r  10378  leexp1a  10379  bernneq  10443  expnbnd  10446  expcan  10494  apexp1  10496  facdiv  10516  faclbnd3  10521  faclbnd6  10522  bcval  10527  bcpasc  10544  bccl  10545  fz1eqb  10569  omgadd  10580  hashunlem  10582  hashfzo  10600  hashfzp1  10602  shftfvalg  10622  shftfval  10625  cjth  10650  remim  10664  reim0b  10666  cjexp  10697  cnrecnv  10714  cvg1nlemcau  10788  cvg1nlemres  10789  recvguniq  10799  resqrexlemp1rp  10810  resqrexlemfp1  10813  resqrexlemlo  10817  resqrexlemgt0  10824  resqrexlemoverl  10825  resqrexlemglsq  10826  resqrexlemsqa  10828  resqrexlemex  10829  resqrex  10830  absexp  10883  recan  10913  climcn2  11110  subcn2  11112  summodc  11184  fsum3  11188  fsum3cvg3  11197  fsumrev  11244  fisum0diag2  11248  telfsumo  11267  fsumrelem  11272  binomlem  11284  binom  11285  binom1dif  11288  bcxmaslem1  11289  bcxmas  11290  isumshft  11291  divcnv  11298  arisum  11299  trireciplem  11301  expcnvap0  11303  expcnvre  11304  expcnv  11305  explecnv  11306  geosergap  11307  geolim  11312  geolim2  11313  geo2sum  11315  geo2lim  11317  geoisum  11318  geoisumr  11319  geoisum1  11320  geoisum1c  11321  cvgratnnlemsumlt  11329  cvgratz  11333  prodmodc  11379  fprodseq  11384  eftvalcn  11400  efcvgfsum  11410  ege2le3  11414  efcj  11416  efaddlem  11417  efexp  11425  eftlub  11433  efgt1p2  11438  eflegeo  11444  sinval  11445  cosval  11446  demoivreALT  11516  divides  11531  dvdscmul  11556  dvds2ln  11562  dvdstr  11566  odd2np1lem  11605  odd2np1  11606  2tp1odd  11617  opeo  11630  omeo  11631  m1expe  11632  m1expo  11633  m1exp1  11634  divalglemnn  11651  divalglemeunn  11654  divalglemeuneg  11656  divalgmod  11660  ndvdssub  11663  gcd0id  11703  bezoutlemnewy  11720  bezoutlema  11723  bezoutlemb  11724  bezoutlemex  11725  bezoutlemaz  11727  bezoutlembz  11728  gcdmultiple  11744  gcdmultiplez  11745  dvdsmulgcd  11749  rplpwr  11751  nn0seqcvgd  11758  dvdslcm  11786  lcmeq0  11788  lcmcl  11789  lcmneg  11791  lcmgcdlem  11794  lcmdvds  11796  lcmid  11797  lcmgcdeq  11800  coprmdvds  11809  mulgcddvds  11811  qredeq  11813  cncongr1  11820  cncongr2  11821  cncongrcoprm  11823  prmind2  11837  isprm6  11861  prmdvdsexp  11862  prmdvdsexpr  11864  sqrt2irr  11876  pw2dvdslemn  11879  pw2dvdseu  11882  oddpwdclemxy  11883  sqpweven  11889  2sqpwodd  11890  sqne2sq  11891  nn0gcdsq  11914  qden1elz  11919  phival  11925  dfphi2  11932  ennnfonelemnn0  11971  ennnfonelemr  11972  txdis1cn  12486  cnmptcom  12506  psmettri2  12536  isxmet2d  12556  xmeteq0  12567  xmettri2  12569  elblps  12598  elbl  12599  blssps  12635  blss  12636  ssblex  12639  blin2  12640  metss2  12706  comet  12707  bdmopn  12712  txmetcnp  12726  blssioo  12753  divcnap  12763  cncfval  12767  cncfi  12773  mulc1cncf  12784  cdivcncfap  12795  mulcncf  12799  expcncf  12800  cnopnap  12802  ellimc3apf  12837  cnlimci  12850  limccnpcntop  12852  limccnp2lem  12853  reldvg  12856  eldvap  12859  dvexp  12883  dvexp2  12884  dvrecap  12885  sin0pilem2  12911  relogbcxpbap  13090  logbgcd1irr  13092  2irrexpq  13101  2irrexpqap  13103  trilpolemclim  13404  trilpolemcl  13405  trilpolemisumle  13406  trilpolemeq1  13408  trilpolemlt1  13409  trilpo  13411  trirec0  13412  redcwlpo  13422  neapmkv  13425