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

Theorem oveq2 5642
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 3618 . . 3  |-  ( A  =  B  ->  <. C ,  A >.  =  <. C ,  B >. )
21fveq2d 5293 . 2  |-  ( A  =  B  ->  ( F `  <. C ,  A >. )  =  ( F `  <. C ,  B >. ) )
3 df-ov 5637 . 2  |-  ( C F A )  =  ( F `  <. C ,  A >. )
4 df-ov 5637 . 2  |-  ( C F B )  =  ( F `  <. C ,  B >. )
52, 3, 43eqtr4g 2145 1  |-  ( A  =  B  ->  ( C F A )  =  ( C F B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1289   <.cop 3444   ` cfv 5002  (class class class)co 5634
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-rex 2365  df-v 2621  df-un 3001  df-sn 3447  df-pr 3448  df-op 3450  df-uni 3649  df-br 3838  df-iota 4967  df-fv 5010  df-ov 5637
This theorem is referenced by:  oveq12  5643  oveq2i  5645  oveq2d  5650  ovanraleqv  5658  rspceov  5673  fovcl  5732  ovmpt2s  5750  ov2gf  5751  ovi3  5763  caovclg  5779  caovcomg  5782  caovassg  5785  caovcang  5788  caovcan  5791  caovordig  5792  caovordg  5794  caovord  5798  caovdig  5801  caovdirg  5804  caovimo  5820  grprinvlem  5821  grprinvd  5822  suppssov1  5835  off  5850  omv  6198  oeiv  6199  oasuc  6207  oawordriexmid  6213  omsuc  6215  nna0r  6221  nnm0r  6222  nnacl  6223  nnmcl  6224  nnacom  6227  nnaass  6228  nndi  6229  nnmass  6230  nnmsucr  6231  nnmcom  6232  nnaordi  6247  nnaord  6248  nnmordi  6255  nnmord  6256  nnaordex  6266  nnawordex  6267  nnm00  6268  eroveu  6363  ecopovtrn  6369  ecopovtrng  6372  th3qlem2  6375  th3q  6377  ecovcom  6379  ecovicom  6380  ecovass  6381  ecoviass  6382  ecovdi  6383  ecovidi  6384  addcanpig  6872  mulcanpig  6873  addcmpblnq  6905  addclnq  6913  mulclnq  6914  recexnq  6928  recmulnqg  6929  ltanqg  6938  ltmnqg  6939  ltexnqq  6946  enq0ref  6971  enq0tr  6972  addcmpblnq0  6981  mulnnnq0  6988  addclnq0  6989  mulclnq0  6990  distrnq0  6997  mulcomnq0  6998  addassnq0  7000  nq02m  7003  prarloclem3  7035  genipv  7047  genpassl  7062  genpassu  7063  addlocpr  7074  distrlem1prl  7120  distrlem1pru  7121  1idprl  7128  1idpru  7129  ltexprlemell  7136  ltexprlemelu  7137  ltexpri  7151  lteupri  7155  ltaprlem  7156  recexprlem1ssl  7171  recexprlem1ssu  7172  recexpr  7176  cauappcvgprlemm  7183  cauappcvgprlemdisj  7189  cauappcvgprlemloc  7190  cauappcvgprlemladdru  7194  cauappcvgprlemladdrl  7195  cauappcvgprlem1  7197  cauappcvgprlemlim  7199  cauappcvgpr  7200  mulcmpblnrlemg  7265  addclsr  7278  mulclsr  7279  ltasrg  7295  negexsr  7297  recexgt0sr  7298  mulgt0sr  7302  mulextsr1  7305  srpospr  7307  caucvgsrlemgt1  7319  axaddrcl  7381  axmulrcl  7383  axaddcom  7384  axrnegex  7393  axprecex  7394  axcnre  7395  axpre-ltadd  7400  axpre-mulgt0  7401  axpre-mulext  7402  rereceu  7403  recriota  7404  axcaucvglemres  7413  readdcan  7601  cnegexlem1  7636  cnegex  7639  addcan  7641  negeq  7654  subadd  7664  addid0  7830  ine0  7851  rimul  8038  cru  8055  apreim  8056  recexap  8096  mulcanapd  8104  receuap  8112  divmulap  8116  cju  8393  nnaddcl  8414  nnmulcl  8415  nnsub  8432  nnnn0addcl  8673  zaddcllempos  8757  zaddcl  8760  zdiv  8804  deceq1  8850  deceq2  8851  uzaddcl  9043  zq  9080  qreccl  9096  cnref1o  9102  fzsuc2  9460  fzrevral  9486  fzshftral  9489  2ffzeq  9517  exfzdc  9616  exbtwnzlemshrink  9625  rebtwn2zlemshrink  9630  modqval  9696  modqmuladd  9738  modqmuladdnn0  9740  frecuzrdgrrn  9780  frec2uzrdg  9781  frecuzrdgrcl  9782  frecuzrdgsuc  9786  frecuzrdgrclt  9787  frecuzrdgg  9788  frecuzrdgsuctlem  9795  frecfzennn  9798  uzsinds  9813  iseqvalcbv  9837  iseqvalt  9838  seq3val  9839  iseqoveq  9850  iseqcaopr3  9875  iseqcaopr2  9876  seq3f1olemp  9896  iseqid  9904  iseqhomo  9907  iseqz  9908  seq3homo  9909  iseqdistr  9910  seq3distr  9911  expp1  9927  expnegap0  9928  expcllem  9931  expcl2lemap  9932  m1expcl2  9942  expap0  9950  mulexp  9959  expadd  9962  expmul  9965  leexp2r  9974  leexp1a  9975  bernneq  10039  expnbnd  10042  expcan  10090  facdiv  10111  faclbnd3  10116  faclbnd6  10117  bcval  10122  bcpasc  10139  bccl  10140  fz1eqb  10164  omgadd  10175  hashunlem  10177  hashfzo  10195  hashfzp1  10197  shftfvalg  10217  shftfval  10220  cjth  10245  remim  10259  reim0b  10261  cjexp  10292  cnrecnv  10309  cvg1nlemcau  10382  cvg1nlemres  10383  recvguniq  10393  resqrexlemp1rp  10404  resqrexlemfp1  10407  resqrexlemlo  10411  resqrexlemgt0  10418  resqrexlemoverl  10419  resqrexlemglsq  10420  resqrexlemsqa  10422  resqrexlemex  10423  resqrex  10424  absexp  10477  recan  10507  climcn2  10662  subcn2  10664  isummo  10737  fisum  10742  fisumcvg3  10752  fsumrev  10800  fisum0diag2  10804  telfsumo  10823  fsumrelem  10828  binomlem  10839  binom  10840  binom1dif  10843  bcxmaslem1  10844  bcxmas  10845  isumshft  10846  divcnv  10852  arisum  10853  trireciplem  10855  expcnvap0  10857  expcnvre  10858  expcnv  10859  explecnv  10860  geosergap  10861  geolim  10866  geolim2  10867  geo2sum  10869  geo2lim  10871  geoisum  10872  geoisumr  10873  geoisum1  10874  geoisum1c  10875  cvgratnnlemsumlt  10883  cvgratz  10887  divides  10891  dvdscmul  10916  dvds2ln  10922  dvdstr  10926  odd2np1lem  10965  odd2np1  10966  2tp1odd  10977  opeo  10990  omeo  10991  m1expe  10992  m1expo  10993  m1exp1  10994  divalglemnn  11011  divalglemeunn  11014  divalglemeuneg  11016  divalgmod  11020  ndvdssub  11023  gcd0id  11063  bezoutlemnewy  11078  bezoutlema  11081  bezoutlemb  11082  bezoutlemex  11083  bezoutlemaz  11085  bezoutlembz  11086  gcdmultiple  11102  gcdmultiplez  11103  dvdsmulgcd  11107  rplpwr  11109  nn0seqcvgd  11116  dvdslcm  11144  lcmeq0  11146  lcmcl  11147  lcmneg  11149  lcmgcdlem  11152  lcmdvds  11154  lcmid  11155  lcmgcdeq  11158  coprmdvds  11167  mulgcddvds  11169  qredeq  11171  cncongr1  11178  cncongr2  11179  cncongrcoprm  11181  prmind2  11195  isprm6  11219  prmdvdsexp  11220  prmdvdsexpr  11222  sqrt2irr  11234  pw2dvdslemn  11236  pw2dvdseu  11239  oddpwdclemxy  11240  sqpweven  11246  2sqpwodd  11247  sqne2sq  11248  nn0gcdsq  11271  qden1elz  11276  phival  11282  dfphi2  11289
  Copyright terms: Public domain W3C validator