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

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

Proof of Theorem oveq2
StepHypRef Expression
1 opeq2 3710 . . 3 (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
21fveq2d 5429 . 2 (𝐴 = 𝐵 → (𝐹‘⟨𝐶, 𝐴⟩) = (𝐹‘⟨𝐶, 𝐵⟩))
3 df-ov 5781 . 2 (𝐶𝐹𝐴) = (𝐹‘⟨𝐶, 𝐴⟩)
4 df-ov 5781 . 2 (𝐶𝐹𝐵) = (𝐹‘⟨𝐶, 𝐵⟩)
52, 3, 43eqtr4g 2198 1 (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1332  cop 3531  cfv 5127  (class class class)co 5778
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 2689  df-un 3076  df-sn 3534  df-pr 3535  df-op 3537  df-uni 3741  df-br 3934  df-iota 5092  df-fv 5135  df-ov 5781
This theorem is referenced by:  oveq12  5787  oveq2i  5789  oveq2d  5794  ovanraleqv  5802  rspceov  5817  fovcl  5880  ovmpos  5898  ov2gf  5899  ovi3  5911  caovclg  5927  caovcomg  5930  caovassg  5933  caovcang  5936  caovcan  5939  caovordig  5940  caovordg  5942  caovord  5946  caovdig  5949  caovdirg  5952  caovimo  5968  grprinvlem  5969  grprinvd  5970  suppssov1  5983  off  5998  omv  6355  oeiv  6356  oasuc  6364  oawordriexmid  6370  omsuc  6372  nna0r  6378  nnm0r  6379  nnacl  6380  nnmcl  6381  nnacom  6384  nnaass  6385  nndi  6386  nnmass  6387  nnmsucr  6388  nnmcom  6389  nnaordi  6408  nnaord  6409  nnmordi  6416  nnmord  6417  nnaordex  6427  nnawordex  6428  nnm00  6429  eroveu  6524  ecopovtrn  6530  ecopovtrng  6533  th3qlem2  6536  th3q  6538  ecovcom  6540  ecovicom  6541  ecovass  6542  ecoviass  6543  ecovdi  6544  ecovidi  6545  addcanpig  7162  mulcanpig  7163  addcmpblnq  7195  addclnq  7203  mulclnq  7204  recexnq  7218  recmulnqg  7219  ltanqg  7228  ltmnqg  7229  ltexnqq  7236  enq0ref  7261  enq0tr  7262  addcmpblnq0  7271  mulnnnq0  7278  addclnq0  7279  mulclnq0  7280  distrnq0  7287  mulcomnq0  7288  addassnq0  7290  nq02m  7293  prarloclem3  7325  genipv  7337  genpassl  7352  genpassu  7353  addlocpr  7364  distrlem1prl  7410  distrlem1pru  7411  1idprl  7418  1idpru  7419  ltexprlemell  7426  ltexprlemelu  7427  ltexpri  7441  lteupri  7445  ltaprlem  7446  recexprlem1ssl  7461  recexprlem1ssu  7462  recexpr  7466  cauappcvgprlemm  7473  cauappcvgprlemdisj  7479  cauappcvgprlemloc  7480  cauappcvgprlemladdru  7484  cauappcvgprlemladdrl  7485  cauappcvgprlem1  7487  cauappcvgprlemlim  7489  cauappcvgpr  7490  mulcmpblnrlemg  7568  addclsr  7581  mulclsr  7582  ltasrg  7598  negexsr  7600  recexgt0sr  7601  mulgt0sr  7606  mulextsr1  7609  srpospr  7611  caucvgsrlemgt1  7623  map2psrprg  7633  axaddrcl  7693  axmulrcl  7695  axaddcom  7698  axrnegex  7707  axprecex  7708  axcnre  7709  axpre-ltadd  7714  axpre-mulgt0  7715  axpre-mulext  7716  rereceu  7717  recriota  7718  axcaucvglemres  7727  readdcan  7922  cnegexlem1  7957  cnegex  7960  addcan  7962  negeq  7975  subadd  7985  addid0  8155  ine0  8176  rimul  8367  cru  8384  apreim  8385  recexap  8434  mulcanapd  8442  receuap  8450  divmulap  8455  cju  8739  nnaddcl  8760  nnmulcl  8761  nnsub  8779  nnnn0addcl  9027  zaddcllempos  9111  zaddcl  9114  zdiv  9159  deceq1  9206  deceq2  9207  uzaddcl  9404  zq  9441  qreccl  9457  cnref1o  9465  xaddnemnf  9666  xaddnepnf  9667  xaddcom  9670  xnn0xadd0  9676  xnegdi  9677  xaddass  9678  xlt2add  9689  xlesubadd  9692  xleaddadd  9696  fzsuc2  9886  fzrevral  9912  fzshftral  9915  2ffzeq  9945  exfzdc  10044  exbtwnzlemshrink  10053  rebtwn2zlemshrink  10058  modqval  10124  modqmuladd  10166  modqmuladdnn0  10168  frecuzrdgrrn  10208  frec2uzrdg  10209  frecuzrdgrcl  10210  frecuzrdgsuc  10214  frecuzrdgrclt  10215  frecuzrdgg  10216  frecuzrdgsuctlem  10223  frecfzennn  10226  uzsinds  10242  iseqvalcbv  10257  seq3val  10258  seqvalcd  10259  seqovcd  10263  seq3caopr3  10281  seq3caopr2  10282  seq3f1olemp  10302  seq3id  10308  seq3homo  10310  seq3z  10311  seq3distr  10313  expp1  10327  expnegap0  10328  expcllem  10331  expcl2lemap  10332  m1expcl2  10342  expap0  10350  mulexp  10359  expadd  10362  expmul  10365  leexp2r  10374  leexp1a  10375  bernneq  10439  expnbnd  10442  expcan  10490  apexp1  10492  facdiv  10512  faclbnd3  10517  faclbnd6  10518  bcval  10523  bcpasc  10540  bccl  10541  fz1eqb  10565  omgadd  10576  hashunlem  10578  hashfzo  10596  hashfzp1  10598  shftfvalg  10618  shftfval  10621  cjth  10646  remim  10660  reim0b  10662  cjexp  10693  cnrecnv  10710  cvg1nlemcau  10784  cvg1nlemres  10785  recvguniq  10795  resqrexlemp1rp  10806  resqrexlemfp1  10809  resqrexlemlo  10813  resqrexlemgt0  10820  resqrexlemoverl  10821  resqrexlemglsq  10822  resqrexlemsqa  10824  resqrexlemex  10825  resqrex  10826  absexp  10879  recan  10909  climcn2  11106  subcn2  11108  summodc  11180  fsum3  11184  fsum3cvg3  11193  fsumrev  11240  fisum0diag2  11244  telfsumo  11263  fsumrelem  11268  binomlem  11280  binom  11281  binom1dif  11284  bcxmaslem1  11285  bcxmas  11286  isumshft  11287  divcnv  11294  arisum  11295  trireciplem  11297  expcnvap0  11299  expcnvre  11300  expcnv  11301  explecnv  11302  geosergap  11303  geolim  11308  geolim2  11309  geo2sum  11311  geo2lim  11313  geoisum  11314  geoisumr  11315  geoisum1  11316  geoisum1c  11317  cvgratnnlemsumlt  11325  cvgratz  11329  prodmodc  11375  eftvalcn  11391  efcvgfsum  11401  ege2le3  11405  efcj  11407  efaddlem  11408  efexp  11416  eftlub  11424  efgt1p2  11429  eflegeo  11435  sinval  11436  cosval  11437  demoivreALT  11507  divides  11522  dvdscmul  11547  dvds2ln  11553  dvdstr  11557  odd2np1lem  11596  odd2np1  11597  2tp1odd  11608  opeo  11621  omeo  11622  m1expe  11623  m1expo  11624  m1exp1  11625  divalglemnn  11642  divalglemeunn  11645  divalglemeuneg  11647  divalgmod  11651  ndvdssub  11654  gcd0id  11694  bezoutlemnewy  11711  bezoutlema  11714  bezoutlemb  11715  bezoutlemex  11716  bezoutlemaz  11718  bezoutlembz  11719  gcdmultiple  11735  gcdmultiplez  11736  dvdsmulgcd  11740  rplpwr  11742  nn0seqcvgd  11749  dvdslcm  11777  lcmeq0  11779  lcmcl  11780  lcmneg  11782  lcmgcdlem  11785  lcmdvds  11787  lcmid  11788  lcmgcdeq  11791  coprmdvds  11800  mulgcddvds  11802  qredeq  11804  cncongr1  11811  cncongr2  11812  cncongrcoprm  11814  prmind2  11828  isprm6  11852  prmdvdsexp  11853  prmdvdsexpr  11855  sqrt2irr  11867  pw2dvdslemn  11870  pw2dvdseu  11873  oddpwdclemxy  11874  sqpweven  11880  2sqpwodd  11881  sqne2sq  11882  nn0gcdsq  11905  qden1elz  11910  phival  11916  dfphi2  11923  ennnfonelemnn0  11962  ennnfonelemr  11963  txdis1cn  12477  cnmptcom  12497  psmettri2  12527  isxmet2d  12547  xmeteq0  12558  xmettri2  12560  elblps  12589  elbl  12590  blssps  12626  blss  12627  ssblex  12630  blin2  12631  metss2  12697  comet  12698  bdmopn  12703  txmetcnp  12717  blssioo  12744  divcnap  12754  cncfval  12758  cncfi  12764  mulc1cncf  12775  cdivcncfap  12786  mulcncf  12790  expcncf  12791  cnopnap  12793  ellimc3apf  12828  cnlimci  12841  limccnpcntop  12843  limccnp2lem  12844  reldvg  12847  eldvap  12850  dvexp  12874  dvexp2  12875  dvrecap  12876  sin0pilem2  12902  relogbcxpbap  13081  logbgcd1irr  13083  trilpolemclim  13387  trilpolemcl  13388  trilpolemisumle  13389  trilpolemeq1  13391  trilpolemlt1  13392  trilpo  13394  trirec0  13395  redcwlpo  13405  neapmkv  13408
  Copyright terms: Public domain W3C validator