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

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

Proof of Theorem oveq2
StepHypRef Expression
1 opeq2 3579 . . 3 (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
21fveq2d 5213 . 2 (𝐴 = 𝐵 → (𝐹‘⟨𝐶, 𝐴⟩) = (𝐹‘⟨𝐶, 𝐵⟩))
3 df-ov 5546 . 2 (𝐶𝐹𝐴) = (𝐹‘⟨𝐶, 𝐴⟩)
4 df-ov 5546 . 2 (𝐶𝐹𝐵) = (𝐹‘⟨𝐶, 𝐵⟩)
52, 3, 43eqtr4g 2139 1 (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1285  cop 3409  cfv 4932  (class class class)co 5543
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 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-rex 2355  df-v 2604  df-un 2978  df-sn 3412  df-pr 3413  df-op 3415  df-uni 3610  df-br 3794  df-iota 4897  df-fv 4940  df-ov 5546
This theorem is referenced by:  oveq12  5552  oveq2i  5554  oveq2d  5559  rspceov  5578  fovcl  5637  ovmpt2s  5655  ov2gf  5656  ovi3  5668  caovclg  5684  caovcomg  5687  caovassg  5690  caovcang  5693  caovcan  5696  caovordig  5697  caovordg  5699  caovord  5703  caovdig  5706  caovdirg  5709  caovimo  5725  grprinvlem  5726  grprinvd  5727  suppssov1  5740  off  5755  omv  6099  oeiv  6100  oasuc  6108  oawordriexmid  6114  omsuc  6116  nna0r  6122  nnm0r  6123  nnacl  6124  nnmcl  6125  nnacom  6128  nnaass  6129  nndi  6130  nnmass  6131  nnmsucr  6132  nnmcom  6133  nnaordi  6147  nnaord  6148  nnmordi  6155  nnmord  6156  nnaordex  6166  nnawordex  6167  nnm00  6168  eroveu  6263  ecopovtrn  6269  ecopovtrng  6272  th3qlem2  6275  th3q  6277  ecovcom  6279  ecovicom  6280  ecovass  6281  ecoviass  6282  ecovdi  6283  ecovidi  6284  addcanpig  6586  mulcanpig  6587  addcmpblnq  6619  addclnq  6627  mulclnq  6628  recexnq  6642  recmulnqg  6643  ltanqg  6652  ltmnqg  6653  ltexnqq  6660  enq0ref  6685  enq0tr  6686  addcmpblnq0  6695  mulnnnq0  6702  addclnq0  6703  mulclnq0  6704  distrnq0  6711  mulcomnq0  6712  addassnq0  6714  nq02m  6717  prarloclem3  6749  genipv  6761  genpassl  6776  genpassu  6777  addlocpr  6788  distrlem1prl  6834  distrlem1pru  6835  1idprl  6842  1idpru  6843  ltexprlemell  6850  ltexprlemelu  6851  ltexpri  6865  lteupri  6869  ltaprlem  6870  recexprlem1ssl  6885  recexprlem1ssu  6886  recexpr  6890  cauappcvgprlemm  6897  cauappcvgprlemdisj  6903  cauappcvgprlemloc  6904  cauappcvgprlemladdru  6908  cauappcvgprlemladdrl  6909  cauappcvgprlem1  6911  cauappcvgprlemlim  6913  cauappcvgpr  6914  mulcmpblnrlemg  6979  addclsr  6992  mulclsr  6993  ltasrg  7009  negexsr  7011  recexgt0sr  7012  mulgt0sr  7016  mulextsr1  7019  srpospr  7021  caucvgsrlemgt1  7033  axaddrcl  7095  axmulrcl  7097  axaddcom  7098  axrnegex  7107  axprecex  7108  axcnre  7109  axpre-ltadd  7114  axpre-mulgt0  7115  axpre-mulext  7116  rereceu  7117  recriota  7118  axcaucvglemres  7127  readdcan  7315  cnegexlem1  7350  cnegex  7353  addcan  7355  negeq  7368  subadd  7378  addid0  7544  ine0  7565  rimul  7752  cru  7769  apreim  7770  recexap  7810  mulcanapd  7818  receuap  7826  divmulap  7830  cju  8105  nnaddcl  8126  nnmulcl  8127  nnsub  8144  nnnn0addcl  8385  zaddcllempos  8469  zaddcl  8472  zdiv  8516  deceq1  8562  deceq2  8563  uzaddcl  8755  zq  8792  qreccl  8808  cnref1o  8814  fzsuc2  9172  fzrevral  9198  fzshftral  9201  2ffzeq  9228  exfzdc  9326  exbtwnzlemshrink  9335  rebtwn2zlemshrink  9340  modqval  9406  modqmuladd  9448  modqmuladdnn0  9450  frecuzrdgrrn  9490  frec2uzrdg  9491  frecuzrdgrcl  9492  frecuzrdgsuc  9496  frecuzrdgrclt  9497  frecuzrdgg  9498  frecuzrdgsuctlem  9505  frecfzennn  9508  uzsinds  9518  iseqvalcbv  9531  iseqvalt  9532  iseqoveq  9540  iseqcaopr3  9556  iseqcaopr2  9557  iseqid  9563  iseqhomo  9565  iseqz  9566  iseqdistr  9567  expp1  9580  expnegap0  9581  expcllem  9584  expcl2lemap  9585  m1expcl2  9595  expap0  9603  mulexp  9612  expadd  9615  expmul  9618  leexp2r  9627  leexp1a  9628  bernneq  9690  expnbnd  9693  expcan  9741  facdiv  9762  faclbnd3  9767  faclbnd6  9768  bcval  9773  bcpasc  9790  bccl  9791  fz1eqb  9815  omgadd  9826  sizeunlem  9828  shftfvalg  9844  shftfval  9847  cjth  9871  remim  9885  reim0b  9887  cjexp  9918  cnrecnv  9935  cvg1nlemcau  10008  cvg1nlemres  10009  recvguniq  10019  resqrexlemp1rp  10030  resqrexlemfp1  10033  resqrexlemlo  10037  resqrexlemgt0  10044  resqrexlemoverl  10045  resqrexlemglsq  10046  resqrexlemsqa  10048  resqrexlemex  10049  resqrex  10050  absexp  10103  recan  10133  climcn2  10286  subcn2  10288  divides  10342  dvdscmul  10367  dvds2ln  10373  dvdstr  10377  odd2np1lem  10416  odd2np1  10417  2tp1odd  10428  opeo  10441  omeo  10442  m1expe  10443  m1expo  10444  m1exp1  10445  divalglemnn  10462  divalglemeunn  10465  divalglemeuneg  10467  divalgmod  10471  ndvdssub  10474  gcd0id  10514  bezoutlemnewy  10529  bezoutlema  10532  bezoutlemb  10533  bezoutlemex  10534  bezoutlemaz  10536  bezoutlembz  10537  gcdmultiple  10553  gcdmultiplez  10554  dvdsmulgcd  10558  rplpwr  10560  nn0seqcvgd  10567  dvdslcm  10595  lcmeq0  10597  lcmcl  10598  lcmneg  10600  lcmgcdlem  10603  lcmdvds  10605  lcmid  10606  lcmgcdeq  10609  coprmdvds  10618  mulgcddvds  10620  qredeq  10622  cncongr1  10629  cncongr2  10630  cncongrcoprm  10632  prmind2  10646  isprm6  10670  prmdvdsexp  10671  prmdvdsexpr  10673  sqrt2irr  10685  pw2dvdslemn  10687  pw2dvdseu  10690  oddpwdclemxy  10691  sqpweven  10697  2sqpwodd  10698  sqne2sq  10699  nn0gcdsq  10722  qden1elz  10727
  Copyright terms: Public domain W3C validator