ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  oveq2 Unicode version

Theorem oveq2 5748
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
StepHypRef Expression
1 opeq2 3674 . . 3  |-  ( A  =  B  ->  <. C ,  A >.  =  <. C ,  B >. )
21fveq2d 5391 . 2  |-  ( A  =  B  ->  ( F `  <. C ,  A >. )  =  ( F `  <. C ,  B >. ) )
3 df-ov 5743 . 2  |-  ( C F A )  =  ( F `  <. C ,  A >. )
4 df-ov 5743 . 2  |-  ( C F B )  =  ( F `  <. C ,  B >. )
52, 3, 43eqtr4g 2173 1  |-  ( A  =  B  ->  ( C F A )  =  ( C F B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1314   <.cop 3498   ` cfv 5091  (class class class)co 5740
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 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-rex 2397  df-v 2660  df-un 3043  df-sn 3501  df-pr 3502  df-op 3504  df-uni 3705  df-br 3898  df-iota 5056  df-fv 5099  df-ov 5743
This theorem is referenced by:  oveq12  5749  oveq2i  5751  oveq2d  5756  ovanraleqv  5764  rspceov  5779  fovcl  5842  ovmpos  5860  ov2gf  5861  ovi3  5873  caovclg  5889  caovcomg  5892  caovassg  5895  caovcang  5898  caovcan  5901  caovordig  5902  caovordg  5904  caovord  5908  caovdig  5911  caovdirg  5914  caovimo  5930  grprinvlem  5931  grprinvd  5932  suppssov1  5945  off  5960  omv  6317  oeiv  6318  oasuc  6326  oawordriexmid  6332  omsuc  6334  nna0r  6340  nnm0r  6341  nnacl  6342  nnmcl  6343  nnacom  6346  nnaass  6347  nndi  6348  nnmass  6349  nnmsucr  6350  nnmcom  6351  nnaordi  6370  nnaord  6371  nnmordi  6378  nnmord  6379  nnaordex  6389  nnawordex  6390  nnm00  6391  eroveu  6486  ecopovtrn  6492  ecopovtrng  6495  th3qlem2  6498  th3q  6500  ecovcom  6502  ecovicom  6503  ecovass  6504  ecoviass  6505  ecovdi  6506  ecovidi  6507  addcanpig  7106  mulcanpig  7107  addcmpblnq  7139  addclnq  7147  mulclnq  7148  recexnq  7162  recmulnqg  7163  ltanqg  7172  ltmnqg  7173  ltexnqq  7180  enq0ref  7205  enq0tr  7206  addcmpblnq0  7215  mulnnnq0  7222  addclnq0  7223  mulclnq0  7224  distrnq0  7231  mulcomnq0  7232  addassnq0  7234  nq02m  7237  prarloclem3  7269  genipv  7281  genpassl  7296  genpassu  7297  addlocpr  7308  distrlem1prl  7354  distrlem1pru  7355  1idprl  7362  1idpru  7363  ltexprlemell  7370  ltexprlemelu  7371  ltexpri  7385  lteupri  7389  ltaprlem  7390  recexprlem1ssl  7405  recexprlem1ssu  7406  recexpr  7410  cauappcvgprlemm  7417  cauappcvgprlemdisj  7423  cauappcvgprlemloc  7424  cauappcvgprlemladdru  7428  cauappcvgprlemladdrl  7429  cauappcvgprlem1  7431  cauappcvgprlemlim  7433  cauappcvgpr  7434  mulcmpblnrlemg  7512  addclsr  7525  mulclsr  7526  ltasrg  7542  negexsr  7544  recexgt0sr  7545  mulgt0sr  7550  mulextsr1  7553  srpospr  7555  caucvgsrlemgt1  7567  map2psrprg  7577  axaddrcl  7637  axmulrcl  7639  axaddcom  7642  axrnegex  7651  axprecex  7652  axcnre  7653  axpre-ltadd  7658  axpre-mulgt0  7659  axpre-mulext  7660  rereceu  7661  recriota  7662  axcaucvglemres  7671  readdcan  7866  cnegexlem1  7901  cnegex  7904  addcan  7906  negeq  7919  subadd  7929  addid0  8099  ine0  8120  rimul  8310  cru  8327  apreim  8328  recexap  8377  mulcanapd  8385  receuap  8393  divmulap  8398  cju  8679  nnaddcl  8700  nnmulcl  8701  nnsub  8719  nnnn0addcl  8961  zaddcllempos  9045  zaddcl  9048  zdiv  9093  deceq1  9140  deceq2  9141  uzaddcl  9333  zq  9370  qreccl  9386  cnref1o  9392  xaddnemnf  9591  xaddnepnf  9592  xaddcom  9595  xnn0xadd0  9601  xnegdi  9602  xaddass  9603  xlt2add  9614  xlesubadd  9617  xleaddadd  9621  fzsuc2  9810  fzrevral  9836  fzshftral  9839  2ffzeq  9869  exfzdc  9968  exbtwnzlemshrink  9977  rebtwn2zlemshrink  9982  modqval  10048  modqmuladd  10090  modqmuladdnn0  10092  frecuzrdgrrn  10132  frec2uzrdg  10133  frecuzrdgrcl  10134  frecuzrdgsuc  10138  frecuzrdgrclt  10139  frecuzrdgg  10140  frecuzrdgsuctlem  10147  frecfzennn  10150  uzsinds  10166  iseqvalcbv  10181  seq3val  10182  seqvalcd  10183  seqovcd  10187  seq3caopr3  10205  seq3caopr2  10206  seq3f1olemp  10226  seq3id  10232  seq3homo  10234  seq3z  10235  seq3distr  10237  expp1  10251  expnegap0  10252  expcllem  10255  expcl2lemap  10256  m1expcl2  10266  expap0  10274  mulexp  10283  expadd  10286  expmul  10289  leexp2r  10298  leexp1a  10299  bernneq  10363  expnbnd  10366  expcan  10414  facdiv  10435  faclbnd3  10440  faclbnd6  10441  bcval  10446  bcpasc  10463  bccl  10464  fz1eqb  10488  omgadd  10499  hashunlem  10501  hashfzo  10519  hashfzp1  10521  shftfvalg  10541  shftfval  10544  cjth  10569  remim  10583  reim0b  10585  cjexp  10616  cnrecnv  10633  cvg1nlemcau  10707  cvg1nlemres  10708  recvguniq  10718  resqrexlemp1rp  10729  resqrexlemfp1  10732  resqrexlemlo  10736  resqrexlemgt0  10743  resqrexlemoverl  10744  resqrexlemglsq  10745  resqrexlemsqa  10747  resqrexlemex  10748  resqrex  10749  absexp  10802  recan  10832  climcn2  11029  subcn2  11031  summodc  11103  fsum3  11107  fsum3cvg3  11116  fsumrev  11163  fisum0diag2  11167  telfsumo  11186  fsumrelem  11191  binomlem  11203  binom  11204  binom1dif  11207  bcxmaslem1  11208  bcxmas  11209  isumshft  11210  divcnv  11217  arisum  11218  trireciplem  11220  expcnvap0  11222  expcnvre  11223  expcnv  11224  explecnv  11225  geosergap  11226  geolim  11231  geolim2  11232  geo2sum  11234  geo2lim  11236  geoisum  11237  geoisumr  11238  geoisum1  11239  geoisum1c  11240  cvgratnnlemsumlt  11248  cvgratz  11252  eftvalcn  11273  efcvgfsum  11283  ege2le3  11287  efcj  11289  efaddlem  11290  efexp  11298  eftlub  11306  efgt1p2  11311  eflegeo  11318  sinval  11319  cosval  11320  demoivreALT  11389  divides  11402  dvdscmul  11427  dvds2ln  11433  dvdstr  11437  odd2np1lem  11476  odd2np1  11477  2tp1odd  11488  opeo  11501  omeo  11502  m1expe  11503  m1expo  11504  m1exp1  11505  divalglemnn  11522  divalglemeunn  11525  divalglemeuneg  11527  divalgmod  11531  ndvdssub  11534  gcd0id  11574  bezoutlemnewy  11591  bezoutlema  11594  bezoutlemb  11595  bezoutlemex  11596  bezoutlemaz  11598  bezoutlembz  11599  gcdmultiple  11615  gcdmultiplez  11616  dvdsmulgcd  11620  rplpwr  11622  nn0seqcvgd  11629  dvdslcm  11657  lcmeq0  11659  lcmcl  11660  lcmneg  11662  lcmgcdlem  11665  lcmdvds  11667  lcmid  11668  lcmgcdeq  11671  coprmdvds  11680  mulgcddvds  11682  qredeq  11684  cncongr1  11691  cncongr2  11692  cncongrcoprm  11694  prmind2  11708  isprm6  11732  prmdvdsexp  11733  prmdvdsexpr  11735  sqrt2irr  11747  pw2dvdslemn  11749  pw2dvdseu  11752  oddpwdclemxy  11753  sqpweven  11759  2sqpwodd  11760  sqne2sq  11761  nn0gcdsq  11784  qden1elz  11789  phival  11795  dfphi2  11802  ennnfonelemnn0  11841  ennnfonelemr  11842  txdis1cn  12353  cnmptcom  12373  psmettri2  12403  isxmet2d  12423  xmeteq0  12434  xmettri2  12436  elblps  12465  elbl  12466  blssps  12502  blss  12503  ssblex  12506  blin2  12507  metss2  12573  comet  12574  bdmopn  12579  txmetcnp  12593  blssioo  12620  divcnap  12630  cncfval  12634  cncfi  12640  mulc1cncf  12651  cdivcncfap  12662  mulcncf  12666  expcncf  12667  cnopnap  12669  ellimc3apf  12704  cnlimci  12717  limccnpcntop  12719  limccnp2lem  12720  reldvg  12723  eldvap  12726  dvexp  12750  dvexp2  12751  dvrecap  12752  trilpolemclim  13063  trilpolemcl  13064  trilpolemisumle  13065  trilpolemeq1  13067  trilpolemlt1  13068  trilpo  13070
  Copyright terms: Public domain W3C validator