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

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

Proof of Theorem oveq2
StepHypRef Expression
1 opeq2 3676 . . 3 (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
21fveq2d 5393 . 2 (𝐴 = 𝐵 → (𝐹‘⟨𝐶, 𝐴⟩) = (𝐹‘⟨𝐶, 𝐵⟩))
3 df-ov 5745 . 2 (𝐶𝐹𝐴) = (𝐹‘⟨𝐶, 𝐴⟩)
4 df-ov 5745 . 2 (𝐶𝐹𝐵) = (𝐹‘⟨𝐶, 𝐵⟩)
52, 3, 43eqtr4g 2175 1 (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1316  cop 3500  cfv 5093  (class class class)co 5742
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 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-3an 949  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-rex 2399  df-v 2662  df-un 3045  df-sn 3503  df-pr 3504  df-op 3506  df-uni 3707  df-br 3900  df-iota 5058  df-fv 5101  df-ov 5745
This theorem is referenced by:  oveq12  5751  oveq2i  5753  oveq2d  5758  ovanraleqv  5766  rspceov  5781  fovcl  5844  ovmpos  5862  ov2gf  5863  ovi3  5875  caovclg  5891  caovcomg  5894  caovassg  5897  caovcang  5900  caovcan  5903  caovordig  5904  caovordg  5906  caovord  5910  caovdig  5913  caovdirg  5916  caovimo  5932  grprinvlem  5933  grprinvd  5934  suppssov1  5947  off  5962  omv  6319  oeiv  6320  oasuc  6328  oawordriexmid  6334  omsuc  6336  nna0r  6342  nnm0r  6343  nnacl  6344  nnmcl  6345  nnacom  6348  nnaass  6349  nndi  6350  nnmass  6351  nnmsucr  6352  nnmcom  6353  nnaordi  6372  nnaord  6373  nnmordi  6380  nnmord  6381  nnaordex  6391  nnawordex  6392  nnm00  6393  eroveu  6488  ecopovtrn  6494  ecopovtrng  6497  th3qlem2  6500  th3q  6502  ecovcom  6504  ecovicom  6505  ecovass  6506  ecoviass  6507  ecovdi  6508  ecovidi  6509  addcanpig  7110  mulcanpig  7111  addcmpblnq  7143  addclnq  7151  mulclnq  7152  recexnq  7166  recmulnqg  7167  ltanqg  7176  ltmnqg  7177  ltexnqq  7184  enq0ref  7209  enq0tr  7210  addcmpblnq0  7219  mulnnnq0  7226  addclnq0  7227  mulclnq0  7228  distrnq0  7235  mulcomnq0  7236  addassnq0  7238  nq02m  7241  prarloclem3  7273  genipv  7285  genpassl  7300  genpassu  7301  addlocpr  7312  distrlem1prl  7358  distrlem1pru  7359  1idprl  7366  1idpru  7367  ltexprlemell  7374  ltexprlemelu  7375  ltexpri  7389  lteupri  7393  ltaprlem  7394  recexprlem1ssl  7409  recexprlem1ssu  7410  recexpr  7414  cauappcvgprlemm  7421  cauappcvgprlemdisj  7427  cauappcvgprlemloc  7428  cauappcvgprlemladdru  7432  cauappcvgprlemladdrl  7433  cauappcvgprlem1  7435  cauappcvgprlemlim  7437  cauappcvgpr  7438  mulcmpblnrlemg  7516  addclsr  7529  mulclsr  7530  ltasrg  7546  negexsr  7548  recexgt0sr  7549  mulgt0sr  7554  mulextsr1  7557  srpospr  7559  caucvgsrlemgt1  7571  map2psrprg  7581  axaddrcl  7641  axmulrcl  7643  axaddcom  7646  axrnegex  7655  axprecex  7656  axcnre  7657  axpre-ltadd  7662  axpre-mulgt0  7663  axpre-mulext  7664  rereceu  7665  recriota  7666  axcaucvglemres  7675  readdcan  7870  cnegexlem1  7905  cnegex  7908  addcan  7910  negeq  7923  subadd  7933  addid0  8103  ine0  8124  rimul  8314  cru  8331  apreim  8332  recexap  8381  mulcanapd  8389  receuap  8397  divmulap  8402  cju  8683  nnaddcl  8704  nnmulcl  8705  nnsub  8723  nnnn0addcl  8965  zaddcllempos  9049  zaddcl  9052  zdiv  9097  deceq1  9144  deceq2  9145  uzaddcl  9337  zq  9374  qreccl  9390  cnref1o  9396  xaddnemnf  9595  xaddnepnf  9596  xaddcom  9599  xnn0xadd0  9605  xnegdi  9606  xaddass  9607  xlt2add  9618  xlesubadd  9621  xleaddadd  9625  fzsuc2  9814  fzrevral  9840  fzshftral  9843  2ffzeq  9873  exfzdc  9972  exbtwnzlemshrink  9981  rebtwn2zlemshrink  9986  modqval  10052  modqmuladd  10094  modqmuladdnn0  10096  frecuzrdgrrn  10136  frec2uzrdg  10137  frecuzrdgrcl  10138  frecuzrdgsuc  10142  frecuzrdgrclt  10143  frecuzrdgg  10144  frecuzrdgsuctlem  10151  frecfzennn  10154  uzsinds  10170  iseqvalcbv  10185  seq3val  10186  seqvalcd  10187  seqovcd  10191  seq3caopr3  10209  seq3caopr2  10210  seq3f1olemp  10230  seq3id  10236  seq3homo  10238  seq3z  10239  seq3distr  10241  expp1  10255  expnegap0  10256  expcllem  10259  expcl2lemap  10260  m1expcl2  10270  expap0  10278  mulexp  10287  expadd  10290  expmul  10293  leexp2r  10302  leexp1a  10303  bernneq  10367  expnbnd  10370  expcan  10418  facdiv  10439  faclbnd3  10444  faclbnd6  10445  bcval  10450  bcpasc  10467  bccl  10468  fz1eqb  10492  omgadd  10503  hashunlem  10505  hashfzo  10523  hashfzp1  10525  shftfvalg  10545  shftfval  10548  cjth  10573  remim  10587  reim0b  10589  cjexp  10620  cnrecnv  10637  cvg1nlemcau  10711  cvg1nlemres  10712  recvguniq  10722  resqrexlemp1rp  10733  resqrexlemfp1  10736  resqrexlemlo  10740  resqrexlemgt0  10747  resqrexlemoverl  10748  resqrexlemglsq  10749  resqrexlemsqa  10751  resqrexlemex  10752  resqrex  10753  absexp  10806  recan  10836  climcn2  11033  subcn2  11035  summodc  11107  fsum3  11111  fsum3cvg3  11120  fsumrev  11167  fisum0diag2  11171  telfsumo  11190  fsumrelem  11195  binomlem  11207  binom  11208  binom1dif  11211  bcxmaslem1  11212  bcxmas  11213  isumshft  11214  divcnv  11221  arisum  11222  trireciplem  11224  expcnvap0  11226  expcnvre  11227  expcnv  11228  explecnv  11229  geosergap  11230  geolim  11235  geolim2  11236  geo2sum  11238  geo2lim  11240  geoisum  11241  geoisumr  11242  geoisum1  11243  geoisum1c  11244  cvgratnnlemsumlt  11252  cvgratz  11256  eftvalcn  11277  efcvgfsum  11287  ege2le3  11291  efcj  11293  efaddlem  11294  efexp  11302  eftlub  11310  efgt1p2  11315  eflegeo  11322  sinval  11323  cosval  11324  demoivreALT  11394  divides  11407  dvdscmul  11432  dvds2ln  11438  dvdstr  11442  odd2np1lem  11481  odd2np1  11482  2tp1odd  11493  opeo  11506  omeo  11507  m1expe  11508  m1expo  11509  m1exp1  11510  divalglemnn  11527  divalglemeunn  11530  divalglemeuneg  11532  divalgmod  11536  ndvdssub  11539  gcd0id  11579  bezoutlemnewy  11596  bezoutlema  11599  bezoutlemb  11600  bezoutlemex  11601  bezoutlemaz  11603  bezoutlembz  11604  gcdmultiple  11620  gcdmultiplez  11621  dvdsmulgcd  11625  rplpwr  11627  nn0seqcvgd  11634  dvdslcm  11662  lcmeq0  11664  lcmcl  11665  lcmneg  11667  lcmgcdlem  11670  lcmdvds  11672  lcmid  11673  lcmgcdeq  11676  coprmdvds  11685  mulgcddvds  11687  qredeq  11689  cncongr1  11696  cncongr2  11697  cncongrcoprm  11699  prmind2  11713  isprm6  11737  prmdvdsexp  11738  prmdvdsexpr  11740  sqrt2irr  11752  pw2dvdslemn  11754  pw2dvdseu  11757  oddpwdclemxy  11758  sqpweven  11764  2sqpwodd  11765  sqne2sq  11766  nn0gcdsq  11789  qden1elz  11794  phival  11800  dfphi2  11807  ennnfonelemnn0  11846  ennnfonelemr  11847  txdis1cn  12358  cnmptcom  12378  psmettri2  12408  isxmet2d  12428  xmeteq0  12439  xmettri2  12441  elblps  12470  elbl  12471  blssps  12507  blss  12508  ssblex  12511  blin2  12512  metss2  12578  comet  12579  bdmopn  12584  txmetcnp  12598  blssioo  12625  divcnap  12635  cncfval  12639  cncfi  12645  mulc1cncf  12656  cdivcncfap  12667  mulcncf  12671  expcncf  12672  cnopnap  12674  ellimc3apf  12709  cnlimci  12722  limccnpcntop  12724  limccnp2lem  12725  reldvg  12728  eldvap  12731  dvexp  12755  dvexp2  12756  dvrecap  12757  sin0pilem2  12774  trilpolemclim  13125  trilpolemcl  13126  trilpolemisumle  13127  trilpolemeq1  13129  trilpolemlt1  13130  trilpo  13132
  Copyright terms: Public domain W3C validator