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

Theorem oveq2 5877
Description: Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
Assertion
Ref Expression
oveq2 (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))

Proof of Theorem oveq2
StepHypRef Expression
1 opeq2 3777 . . 3 (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
21fveq2d 5515 . 2 (𝐴 = 𝐵 → (𝐹‘⟨𝐶, 𝐴⟩) = (𝐹‘⟨𝐶, 𝐵⟩))
3 df-ov 5872 . 2 (𝐶𝐹𝐴) = (𝐹‘⟨𝐶, 𝐴⟩)
4 df-ov 5872 . 2 (𝐶𝐹𝐵) = (𝐹‘⟨𝐶, 𝐵⟩)
52, 3, 43eqtr4g 2235 1 (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1353  cop 3594  cfv 5212  (class class class)co 5869
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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2739  df-un 3133  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-br 4001  df-iota 5174  df-fv 5220  df-ov 5872
This theorem is referenced by:  oveq12  5878  oveq2i  5880  oveq2d  5885  ovanraleqv  5893  ovrspc2v  5895  oveqrspc2v  5896  rspceov  5911  fovcl  5974  ovmpos  5992  ov2gf  5993  ovi3  6005  caovclg  6021  caovcomg  6024  caovassg  6027  caovcang  6030  caovcan  6033  caovordig  6034  caovordg  6036  caovord  6040  caovdig  6043  caovdirg  6046  caovimo  6062  suppssov1  6074  off  6089  omv  6450  oeiv  6451  oasuc  6459  oawordriexmid  6465  omsuc  6467  nna0r  6473  nnm0r  6474  nnacl  6475  nnmcl  6476  nnacom  6479  nnaass  6480  nndi  6481  nnmass  6482  nnmsucr  6483  nnmcom  6484  nnaordi  6503  nnaord  6504  nnmordi  6511  nnmord  6512  nnaordex  6523  nnawordex  6524  nnm00  6525  eroveu  6620  ecopovtrn  6626  ecopovtrng  6629  th3qlem2  6632  th3q  6634  ecovcom  6636  ecovicom  6637  ecovass  6638  ecoviass  6639  ecovdi  6640  ecovidi  6641  addcanpig  7321  mulcanpig  7322  addcmpblnq  7354  addclnq  7362  mulclnq  7363  recexnq  7377  recmulnqg  7378  ltanqg  7387  ltmnqg  7388  ltexnqq  7395  enq0ref  7420  enq0tr  7421  addcmpblnq0  7430  mulnnnq0  7437  addclnq0  7438  mulclnq0  7439  distrnq0  7446  mulcomnq0  7447  addassnq0  7449  nq02m  7452  prarloclem3  7484  genipv  7496  genpassl  7511  genpassu  7512  addlocpr  7523  distrlem1prl  7569  distrlem1pru  7570  1idprl  7577  1idpru  7578  ltexprlemell  7585  ltexprlemelu  7586  ltexpri  7600  lteupri  7604  ltaprlem  7605  recexprlem1ssl  7620  recexprlem1ssu  7621  recexpr  7625  cauappcvgprlemm  7632  cauappcvgprlemdisj  7638  cauappcvgprlemloc  7639  cauappcvgprlemladdru  7643  cauappcvgprlemladdrl  7644  cauappcvgprlem1  7646  cauappcvgprlemlim  7648  cauappcvgpr  7649  mulcmpblnrlemg  7727  addclsr  7740  mulclsr  7741  ltasrg  7757  negexsr  7759  recexgt0sr  7760  mulgt0sr  7765  mulextsr1  7768  srpospr  7770  caucvgsrlemgt1  7782  map2psrprg  7792  axaddrcl  7852  axmulrcl  7854  axaddcom  7857  axrnegex  7866  axprecex  7867  axcnre  7868  axpre-ltadd  7873  axpre-mulgt0  7874  axpre-mulext  7875  rereceu  7876  recriota  7877  axcaucvglemres  7886  readdcan  8084  cnegexlem1  8119  cnegex  8122  addcan  8124  negeq  8137  subadd  8147  addid0  8317  ine0  8338  rimul  8529  cru  8546  apreim  8547  recexap  8596  mulcanapd  8604  receuap  8612  divmulap  8618  rerecapb  8786  cju  8904  nnaddcl  8925  nnmulcl  8926  nnsub  8944  nnnn0addcl  9192  zaddcllempos  9276  zaddcl  9279  zdiv  9327  deceq1  9374  deceq2  9375  uzaddcl  9572  zq  9612  qreccl  9628  cnref1o  9636  xaddnemnf  9841  xaddnepnf  9842  xaddcom  9845  xnn0xadd0  9851  xnegdi  9852  xaddass  9853  xlt2add  9864  xlesubadd  9867  xleaddadd  9871  fzsuc2  10062  fzrevral  10088  fzshftral  10091  2ffzeq  10124  exfzdc  10223  exbtwnzlemshrink  10232  rebtwn2zlemshrink  10237  modqval  10307  modqmuladd  10349  modqmuladdnn0  10351  frecuzrdgrrn  10391  frec2uzrdg  10392  frecuzrdgrcl  10393  frecuzrdgsuc  10397  frecuzrdgrclt  10398  frecuzrdgg  10399  frecuzrdgsuctlem  10406  frecfzennn  10409  uzsinds  10425  iseqvalcbv  10440  seq3val  10441  seqvalcd  10442  seqovcd  10446  seq3caopr3  10464  seq3caopr2  10465  seq3f1olemp  10485  seq3id  10491  seq3homo  10493  seq3z  10494  seq3distr  10496  expp1  10510  expnegap0  10511  expcllem  10514  expcl2lemap  10515  m1expcl2  10525  expap0  10533  mulexp  10542  expadd  10545  expmul  10548  leexp2r  10557  leexp1a  10558  bernneq  10623  expnbnd  10626  modqexp  10629  nn0ltexp2  10671  expcan  10677  apexp1  10679  facdiv  10699  faclbnd3  10704  faclbnd6  10705  bcval  10710  bcpasc  10727  bccl  10728  fz1eqb  10751  omgadd  10763  hashunlem  10765  hashfzo  10783  hashfzp1  10785  shftfvalg  10808  shftfval  10811  cjth  10836  remim  10850  reim0b  10852  cjexp  10883  cnrecnv  10900  cvg1nlemcau  10974  cvg1nlemres  10975  recvguniq  10985  resqrexlemp1rp  10996  resqrexlemfp1  10999  resqrexlemlo  11003  resqrexlemgt0  11010  resqrexlemoverl  11011  resqrexlemglsq  11012  resqrexlemsqa  11014  resqrexlemex  11015  resqrex  11016  absexp  11069  recan  11099  climcn2  11298  subcn2  11300  summodc  11372  fsum3  11376  fsum3cvg3  11385  fsumrev  11432  fisum0diag2  11436  telfsumo  11455  fsumrelem  11460  binomlem  11472  binom  11473  binom1dif  11476  bcxmaslem1  11477  bcxmas  11478  isumshft  11479  divcnv  11486  arisum  11487  trireciplem  11489  expcnvap0  11491  expcnvre  11492  expcnv  11493  explecnv  11494  geosergap  11495  geolim  11500  geolim2  11501  geo2sum  11503  geo2lim  11505  geoisum  11506  geoisumr  11507  geoisum1  11508  geoisum1c  11509  cvgratnnlemsumlt  11517  cvgratz  11521  prodmodc  11567  fprodseq  11572  fprodcl2lem  11594  fprodfac  11604  fprodabs  11605  fprodrev  11608  eftvalcn  11646  efcvgfsum  11656  ege2le3  11660  efcj  11662  efaddlem  11663  efexp  11671  eftlub  11679  efgt1p2  11684  eflegeo  11690  sinval  11691  cosval  11692  demoivreALT  11762  divides  11777  dvdscmul  11806  dvds2ln  11812  dvdstr  11816  odd2np1lem  11857  odd2np1  11858  2tp1odd  11869  opeo  11882  omeo  11883  m1expe  11884  m1expo  11885  m1exp1  11886  divalglemnn  11903  divalglemeunn  11906  divalglemeuneg  11908  divalgmod  11912  ndvdssub  11915  gcd0id  11960  bezoutlemnewy  11977  bezoutlema  11980  bezoutlemb  11981  bezoutlemex  11982  bezoutlemaz  11984  bezoutlembz  11985  gcdmultiple  12001  gcdmultiplez  12002  dvdsmulgcd  12006  rplpwr  12008  nn0seqcvgd  12021  dvdslcm  12049  lcmeq0  12051  lcmcl  12052  lcmneg  12054  lcmgcdlem  12057  lcmdvds  12059  lcmid  12060  lcmgcdeq  12063  coprmdvds  12072  mulgcddvds  12074  qredeq  12076  cncongr1  12083  cncongr2  12084  cncongrcoprm  12086  prmind2  12100  isprm6  12127  prmdvdsexp  12128  prmdvdsexpr  12130  sqrt2irr  12142  pw2dvdslemn  12145  pw2dvdseu  12148  oddpwdclemxy  12149  sqpweven  12155  2sqpwodd  12156  sqne2sq  12157  nn0gcdsq  12180  qden1elz  12185  phival  12193  dfphi2  12200  eulerthlemrprm  12209  eulerthlema  12210  prmdiv  12215  prmdiveq  12216  phisum  12220  odzval  12221  odzcllem  12222  odzdvds  12225  reumodprminv  12233  pythagtriplem3  12247  pythagtriplem18  12261  pythagtriplem19  12262  pclem0  12266  pclemub  12267  pclemdc  12268  pcprecl  12269  pcprendvds  12270  pcpremul  12273  pceulem  12274  pceu  12275  pczpre  12277  pcdiv  12282  pcqmul  12283  pcqcl  12286  pcexp  12289  pcxnn0cl  12290  pcxcl  12291  pcge0  12292  pcdvdsb  12299  pcneg  12304  pcabs  12305  pcgcd1  12307  pc2dvds  12309  pc11  12310  pcz  12311  pcprmpw2  12312  pcprmpw  12313  dvdsprmpweq  12314  dvdsprmpweqnn  12315  dvdsprmpweqle  12316  pcaddlem  12318  pcadd  12319  pcfac  12328  oddprmdvds  12332  prmpwdvds  12333  pockthi  12336  infpnlem2  12338  1arithlem1  12341  ennnfonelemnn0  12403  ennnfonelemr  12404  mgm1  12678  mgmidmo  12680  mgmlrid  12687  lidrideqd  12689  lidrididd  12690  grprinvlem  12693  grprinvd  12694  isnsgrp  12701  sgrpass  12703  sgrp1  12705  mndinvmod  12733  mnd1  12734  mnd1id  12735  mhmpropd  12744  mhmlin  12745  insubm  12759  mhmima  12762  grpinvex  12774  grppropd  12780  dfgrp2  12789  grpidd2  12801  grpinvval  12803  grpinvid1  12811  grplrinv  12814  grpidinv2  12815  grpidinv  12816  grplcan  12818  grpidssd  12832  grpinvssd  12833  dfgrp3mlem  12854  dfgrp3m  12855  grplactcnv  12858  grp1  12862  mhmlem  12864  mulginvcom  12893  mulgnn0ass  12904  mulgmodid  12907  srglz  12991  srgisid  12992  srglmhm  12999  ringid  13032  ringinvnz1ne0  13049  ringinvnzdiv  13050  ring1  13059  dvdsrtr  13092  txdis1cn  13438  cnmptcom  13458  psmettri2  13488  isxmet2d  13508  xmeteq0  13519  xmettri2  13521  elblps  13550  elbl  13551  blssps  13587  blss  13588  ssblex  13591  blin2  13592  metss2  13658  comet  13659  bdmopn  13664  txmetcnp  13678  blssioo  13705  divcnap  13715  cncfval  13719  cncfi  13725  mulc1cncf  13736  cdivcncfap  13747  mulcncf  13751  expcncf  13752  cnopnap  13754  ellimc3apf  13789  cnlimci  13802  limccnpcntop  13804  limccnp2lem  13805  reldvg  13808  eldvap  13811  dvexp  13835  dvexp2  13836  dvrecap  13837  sin0pilem2  13863  relogbcxpbap  14043  logbgcd1irr  14045  2irrexpq  14054  2irrexpqap  14056  lgsneg  14085  lgsdilem  14088  lgsdir  14096  lgsdilem2  14097  lgsdi  14098  lgsne0  14099  lgsdirnn0  14108  lgsdinn0  14109  2sqlem6  14116  2sqlem8  14119  2sqlem9  14120  2sqlem10  14121  trilpolemclim  14433  trilpolemcl  14434  trilpolemisumle  14435  trilpolemeq1  14437  trilpolemlt1  14438  trilpo  14440  trirec0  14441  redcwlpo  14452  nconstwlpolemgt0  14460  nconstwlpo  14462  neapmkv  14464
  Copyright terms: Public domain W3C validator