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

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

Proof of Theorem oveq2
StepHypRef Expression
1 opeq2 3606 . . 3 (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
21fveq2d 5272 . 2 (𝐴 = 𝐵 → (𝐹‘⟨𝐶, 𝐴⟩) = (𝐹‘⟨𝐶, 𝐵⟩))
3 df-ov 5616 . 2 (𝐶𝐹𝐴) = (𝐹‘⟨𝐶, 𝐴⟩)
4 df-ov 5616 . 2 (𝐶𝐹𝐵) = (𝐹‘⟨𝐶, 𝐵⟩)
52, 3, 43eqtr4g 2142 1 (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1287  cop 3434  cfv 4981  (class class class)co 5613
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 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-rex 2361  df-v 2617  df-un 2992  df-sn 3437  df-pr 3438  df-op 3440  df-uni 3637  df-br 3821  df-iota 4946  df-fv 4989  df-ov 5616
This theorem is referenced by:  oveq12  5622  oveq2i  5624  oveq2d  5629  rspceov  5648  fovcl  5707  ovmpt2s  5725  ov2gf  5726  ovi3  5738  caovclg  5754  caovcomg  5757  caovassg  5760  caovcang  5763  caovcan  5766  caovordig  5767  caovordg  5769  caovord  5773  caovdig  5776  caovdirg  5779  caovimo  5795  grprinvlem  5796  grprinvd  5797  suppssov1  5810  off  5825  omv  6170  oeiv  6171  oasuc  6179  oawordriexmid  6185  omsuc  6187  nna0r  6193  nnm0r  6194  nnacl  6195  nnmcl  6196  nnacom  6199  nnaass  6200  nndi  6201  nnmass  6202  nnmsucr  6203  nnmcom  6204  nnaordi  6219  nnaord  6220  nnmordi  6227  nnmord  6228  nnaordex  6238  nnawordex  6239  nnm00  6240  eroveu  6335  ecopovtrn  6341  ecopovtrng  6344  th3qlem2  6347  th3q  6349  ecovcom  6351  ecovicom  6352  ecovass  6353  ecoviass  6354  ecovdi  6355  ecovidi  6356  addcanpig  6837  mulcanpig  6838  addcmpblnq  6870  addclnq  6878  mulclnq  6879  recexnq  6893  recmulnqg  6894  ltanqg  6903  ltmnqg  6904  ltexnqq  6911  enq0ref  6936  enq0tr  6937  addcmpblnq0  6946  mulnnnq0  6953  addclnq0  6954  mulclnq0  6955  distrnq0  6962  mulcomnq0  6963  addassnq0  6965  nq02m  6968  prarloclem3  7000  genipv  7012  genpassl  7027  genpassu  7028  addlocpr  7039  distrlem1prl  7085  distrlem1pru  7086  1idprl  7093  1idpru  7094  ltexprlemell  7101  ltexprlemelu  7102  ltexpri  7116  lteupri  7120  ltaprlem  7121  recexprlem1ssl  7136  recexprlem1ssu  7137  recexpr  7141  cauappcvgprlemm  7148  cauappcvgprlemdisj  7154  cauappcvgprlemloc  7155  cauappcvgprlemladdru  7159  cauappcvgprlemladdrl  7160  cauappcvgprlem1  7162  cauappcvgprlemlim  7164  cauappcvgpr  7165  mulcmpblnrlemg  7230  addclsr  7243  mulclsr  7244  ltasrg  7260  negexsr  7262  recexgt0sr  7263  mulgt0sr  7267  mulextsr1  7270  srpospr  7272  caucvgsrlemgt1  7284  axaddrcl  7346  axmulrcl  7348  axaddcom  7349  axrnegex  7358  axprecex  7359  axcnre  7360  axpre-ltadd  7365  axpre-mulgt0  7366  axpre-mulext  7367  rereceu  7368  recriota  7369  axcaucvglemres  7378  readdcan  7566  cnegexlem1  7601  cnegex  7604  addcan  7606  negeq  7619  subadd  7629  addid0  7795  ine0  7816  rimul  8003  cru  8020  apreim  8021  recexap  8061  mulcanapd  8069  receuap  8077  divmulap  8081  cju  8356  nnaddcl  8377  nnmulcl  8378  nnsub  8395  nnnn0addcl  8636  zaddcllempos  8720  zaddcl  8723  zdiv  8767  deceq1  8813  deceq2  8814  uzaddcl  9006  zq  9043  qreccl  9059  cnref1o  9065  fzsuc2  9423  fzrevral  9449  fzshftral  9452  2ffzeq  9480  exfzdc  9579  exbtwnzlemshrink  9588  rebtwn2zlemshrink  9593  modqval  9659  modqmuladd  9701  modqmuladdnn0  9703  frecuzrdgrrn  9743  frec2uzrdg  9744  frecuzrdgrcl  9745  frecuzrdgsuc  9749  frecuzrdgrclt  9750  frecuzrdgg  9751  frecuzrdgsuctlem  9758  frecfzennn  9761  uzsinds  9776  iseqvalcbv  9789  iseqvalt  9790  iseqoveq  9799  iseqcaopr3  9815  iseqcaopr2  9816  iseqf1olemp  9836  iseqid  9843  iseqhomo  9845  iseqz  9846  iseqdistr  9847  expp1  9861  expnegap0  9862  expcllem  9865  expcl2lemap  9866  m1expcl2  9876  expap0  9884  mulexp  9893  expadd  9896  expmul  9899  leexp2r  9908  leexp1a  9909  bernneq  9971  expnbnd  9974  expcan  10022  facdiv  10043  faclbnd3  10048  faclbnd6  10049  bcval  10054  bcpasc  10071  bccl  10072  fz1eqb  10096  omgadd  10107  hashunlem  10109  hashfzo  10127  hashfzp1  10129  shftfvalg  10149  shftfval  10152  cjth  10176  remim  10190  reim0b  10192  cjexp  10223  cnrecnv  10240  cvg1nlemcau  10313  cvg1nlemres  10314  recvguniq  10324  resqrexlemp1rp  10335  resqrexlemfp1  10338  resqrexlemlo  10342  resqrexlemgt0  10349  resqrexlemoverl  10350  resqrexlemglsq  10351  resqrexlemsqa  10353  resqrexlemex  10354  resqrex  10355  absexp  10408  recan  10438  climcn2  10592  subcn2  10594  isummo  10664  fisum  10667  fisumcvg3  10676  divides  10680  dvdscmul  10705  dvds2ln  10711  dvdstr  10715  odd2np1lem  10754  odd2np1  10755  2tp1odd  10766  opeo  10779  omeo  10780  m1expe  10781  m1expo  10782  m1exp1  10783  divalglemnn  10800  divalglemeunn  10803  divalglemeuneg  10805  divalgmod  10809  ndvdssub  10812  gcd0id  10852  bezoutlemnewy  10867  bezoutlema  10870  bezoutlemb  10871  bezoutlemex  10872  bezoutlemaz  10874  bezoutlembz  10875  gcdmultiple  10891  gcdmultiplez  10892  dvdsmulgcd  10896  rplpwr  10898  nn0seqcvgd  10905  dvdslcm  10933  lcmeq0  10935  lcmcl  10936  lcmneg  10938  lcmgcdlem  10941  lcmdvds  10943  lcmid  10944  lcmgcdeq  10947  coprmdvds  10956  mulgcddvds  10958  qredeq  10960  cncongr1  10967  cncongr2  10968  cncongrcoprm  10970  prmind2  10984  isprm6  11008  prmdvdsexp  11009  prmdvdsexpr  11011  sqrt2irr  11023  pw2dvdslemn  11025  pw2dvdseu  11028  oddpwdclemxy  11029  sqpweven  11035  2sqpwodd  11036  sqne2sq  11037  nn0gcdsq  11060  qden1elz  11065  phival  11071  dfphi2  11078
  Copyright terms: Public domain W3C validator