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

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

Proof of Theorem oveq1
StepHypRef Expression
1 opeq1 3549 . . 3 (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
21fveq2d 5182 . 2 (𝐴 = 𝐵 → (𝐹‘⟨𝐴, 𝐶⟩) = (𝐹‘⟨𝐵, 𝐶⟩))
3 df-ov 5515 . 2 (𝐴𝐹𝐶) = (𝐹‘⟨𝐴, 𝐶⟩)
4 df-ov 5515 . 2 (𝐵𝐹𝐶) = (𝐹‘⟨𝐵, 𝐶⟩)
52, 3, 43eqtr4g 2097 1 (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1243  cop 3378  cfv 4902  (class class class)co 5512
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-rex 2312  df-v 2559  df-un 2922  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-br 3765  df-iota 4867  df-fv 4910  df-ov 5515
This theorem is referenced by:  oveq12  5521  oveq1i  5522  oveq1d  5527  rspceov  5547  fovcl  5606  ovmpt2s  5624  ov2gf  5625  ovi3  5637  caovclg  5653  caovcomg  5656  caovassg  5659  caovcang  5662  caovcan  5665  caovordig  5666  caovordg  5668  caovord  5672  caovdig  5675  caovdirg  5678  caovimo  5694  grpridd  5697  suppssov1  5709  off  5724  omcl  6041  oeicl  6042  omv2  6045  nnm0r  6058  nnacom  6063  nndi  6065  nnmass  6066  nnmsucr  6067  nnmcom  6068  nnaword  6084  nnmord  6090  nnm00  6102  eroveu  6197  th3qlem2  6209  th3q  6211  ecovcom  6213  ecovicom  6214  ecovass  6215  ecoviass  6216  ecovdi  6217  ecovidi  6218  addcmpblnq  6465  addclnq  6473  mulclnq  6474  mulidnq  6487  recexnq  6488  recmulnqg  6489  ltanqg  6498  ltmnqg  6499  ltexnqq  6506  enq0ref  6531  enq0tr  6532  addcmpblnq0  6541  mulnnnq0  6548  addclnq0  6549  mulclnq0  6550  distrnq0  6557  mulcomnq0  6558  addassnq0  6560  prarloclemlo  6592  prarloclem3  6595  prarloclem5  6598  prarloclemcalc  6600  genipv  6607  genpassl  6622  genpassu  6623  addlocprlemeq  6631  distrlem4prl  6682  distrlem4pru  6683  ltexprlemdisj  6704  ltexprlemloc  6705  ltexprlemrl  6708  ltexprlemru  6710  prplnqu  6718  cauappcvgprlemm  6743  cauappcvgprlemopl  6744  cauappcvgprlemlol  6745  cauappcvgprlemdisj  6749  cauappcvgprlemloc  6750  cauappcvgprlemladdfl  6753  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  cauappcvgprlem1  6757  cauappcvgprlemlim  6759  cauappcvgpr  6760  caucvgprlemm  6766  caucvgprlemopl  6767  caucvgprlemlol  6768  caucvgprlemdisj  6772  caucvgprlemloc  6773  caucvgprlemladdrl  6776  caucvgprlem1  6777  caucvgpr  6780  caucvgprprlemell  6783  caucvgprprlemml  6792  caucvgprpr  6810  mulcmpblnrlemg  6825  addclsr  6838  mulclsr  6839  0idsr  6852  1idsr  6853  00sr  6854  ltasrg  6855  recexgt0sr  6858  mulgt0sr  6862  mulextsr1  6865  prsrriota  6872  caucvgsrlemgt1  6879  caucvgsrlemoffres  6884  pitonn  6924  peano2nnnn  6929  axaddrcl  6941  axmulrcl  6943  axaddcom  6944  ax1rid  6951  ax0id  6952  axprecex  6954  axcnre  6955  axpre-ltadd  6960  axpre-mulgt0  6961  axpre-mulext  6962  rereceu  6963  peano5nnnn  6966  axcaucvglemcau  6972  axcaucvglemres  6973  mulid1  7024  cnegexlem1  7186  cnegexlem2  7187  cnegex  7189  addcan2  7192  subval  7203  apreim  7594  recexap  7634  receuap  7650  divvalap  7653  cju  7913  peano2nn  7926  nn1m1nn  7932  nn1suc  7933  nnsub  7952  nnm1nn0  8223  zdiv  8328  zneo  8339  nneoor  8340  zeo  8343  peano5uzti  8346  nn0ind-raph  8355  uzind4s  8533  uzind4s2  8534  qmulz  8558  cnref1o  8582  fzsuc2  8941  fzm1  8962  fzoval  9005  qbtwnzlemstep  9103  qbtwnzlemshrink  9104  qbtwnzlemex  9105  qbtwnz  9106  rebtwn2zlemstep  9107  rebtwn2zlemshrink  9108  rebtwn2z  9109  flqlelt  9118  flqbi  9132  fldiv4p1lem1div2  9147  modqval  9166  frec2uzzd  9186  frec2uzsucd  9187  frec2uzrand  9191  frecuzrdgrrn  9194  frec2uzrdg  9195  frecuzrdgsuc  9201  iseqval  9220  iseqp1  9225  iseqss  9226  iseqfveq2  9228  iseqshft2  9232  monoord  9235  monoord2  9236  iseqsplit  9238  iseqcaopr3  9240  iseqcaopr2  9241  iseqhomo  9248  iseqdistr  9249  m1expcl2  9277  mulexp  9294  expadd  9297  expmul  9300  sq0i  9345  shftlem  9417  shftfvalg  9419  shftfibg  9421  shftfval  9422  shftfib  9424  shftfn  9425  shftf  9431  2shfti  9432  shftvalg  9437  shftval4g  9438  cjval  9445  imval  9450  cjexp  9493  cnrecnv  9510  cvg1nlemcau  9583  cvg1nlemres  9584  resqrexlemcalc3  9614  resqrexlemex  9623  rsqrmo  9625  resqrtcl  9627  rersqrtthlem  9628  sqrtsq  9642  absexp  9675  recan  9705  climshft  9825  climcn1  9829  climcn2  9830  subcn2  9832  serif0  9871  sqrt2irr  9878  qdencn  10124
  Copyright terms: Public domain W3C validator