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

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

Proof of Theorem oveq1
StepHypRef Expression
1 opeq1 3599 . . 3 (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
21fveq2d 5260 . 2 (𝐴 = 𝐵 → (𝐹‘⟨𝐴, 𝐶⟩) = (𝐹‘⟨𝐵, 𝐶⟩))
3 df-ov 5597 . 2 (𝐴𝐹𝐶) = (𝐹‘⟨𝐴, 𝐶⟩)
4 df-ov 5597 . 2 (𝐵𝐹𝐶) = (𝐹‘⟨𝐵, 𝐶⟩)
52, 3, 43eqtr4g 2142 1 (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1287  cop 3428  cfv 4972  (class class class)co 5594
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 2616  df-un 2990  df-sn 3431  df-pr 3432  df-op 3434  df-uni 3631  df-br 3815  df-iota 4937  df-fv 4980  df-ov 5597
This theorem is referenced by:  oveq12  5603  oveq1i  5604  oveq1d  5609  rspceov  5629  fovcl  5688  ovmpt2s  5706  ov2gf  5707  ovi3  5719  caovclg  5735  caovcomg  5738  caovassg  5741  caovcang  5744  caovcan  5747  caovordig  5748  caovordg  5750  caovord  5754  caovdig  5757  caovdirg  5760  caovimo  5776  grpridd  5779  suppssov1  5791  off  5806  omcl  6157  oeicl  6158  omv2  6161  nnm0r  6175  nnacom  6180  nndi  6182  nnmass  6183  nnmsucr  6184  nnmcom  6185  nnaword  6203  nnmord  6209  nnm00  6221  eroveu  6316  th3qlem2  6328  th3q  6330  ecovcom  6332  ecovicom  6333  ecovass  6334  ecoviass  6335  ecovdi  6336  ecovidi  6337  map0g  6378  addcmpblnq  6847  addclnq  6855  mulclnq  6856  mulidnq  6869  recexnq  6870  recmulnqg  6871  ltanqg  6880  ltmnqg  6881  ltexnqq  6888  enq0ref  6913  enq0tr  6914  addcmpblnq0  6923  mulnnnq0  6930  addclnq0  6931  mulclnq0  6932  distrnq0  6939  mulcomnq0  6940  addassnq0  6942  prarloclemlo  6974  prarloclem3  6977  prarloclem5  6980  prarloclemcalc  6982  genipv  6989  genpassl  7004  genpassu  7005  addlocprlemeq  7013  distrlem4prl  7064  distrlem4pru  7065  ltexprlemdisj  7086  ltexprlemloc  7087  ltexprlemrl  7090  ltexprlemru  7092  prplnqu  7100  cauappcvgprlemm  7125  cauappcvgprlemopl  7126  cauappcvgprlemlol  7127  cauappcvgprlemdisj  7131  cauappcvgprlemloc  7132  cauappcvgprlemladdfl  7135  cauappcvgprlemladdru  7136  cauappcvgprlemladdrl  7137  cauappcvgprlem1  7139  cauappcvgprlemlim  7141  cauappcvgpr  7142  caucvgprlemm  7148  caucvgprlemopl  7149  caucvgprlemlol  7150  caucvgprlemdisj  7154  caucvgprlemloc  7155  caucvgprlemladdrl  7158  caucvgprlem1  7159  caucvgpr  7162  caucvgprprlemell  7165  caucvgprprlemml  7174  caucvgprpr  7192  mulcmpblnrlemg  7207  addclsr  7220  mulclsr  7221  0idsr  7234  1idsr  7235  00sr  7236  ltasrg  7237  recexgt0sr  7240  mulgt0sr  7244  mulextsr1  7247  prsrriota  7254  caucvgsrlemgt1  7261  caucvgsrlemoffres  7266  pitonn  7306  peano2nnnn  7311  axaddrcl  7323  axmulrcl  7325  axaddcom  7326  ax1rid  7333  ax0id  7334  axprecex  7336  axcnre  7337  axpre-ltadd  7342  axpre-mulgt0  7343  axpre-mulext  7344  rereceu  7345  peano5nnnn  7348  axcaucvglemcau  7354  axcaucvglemres  7355  mulid1  7406  cnegexlem1  7578  cnegexlem2  7579  cnegex  7581  addcan2  7584  subval  7595  addlsub  7769  apreim  7998  recexap  8038  receuap  8054  divvalap  8057  cju  8333  peano2nn  8346  nn1m1nn  8352  nn1suc  8353  nnsub  8372  nnm1nn0  8624  zdiv  8744  zneo  8757  nneoor  8758  zeo  8761  peano5uzti  8764  nn0ind-raph  8773  uzind4s  8987  uzind4s2  8988  qmulz  9017  cnref1o  9042  nn0ledivnn  9147  fzsuc2  9400  fzm1  9421  fzoval  9463  exbtwnzlemstep  9562  exbtwnzlemshrink  9563  exbtwnzlemex  9564  exbtwnz  9565  rebtwn2zlemstep  9567  rebtwn2zlemshrink  9568  rebtwn2z  9569  flqlelt  9586  flqbi  9600  fldiv4p1lem1div2  9615  modqval  9634  modqadd1  9671  modqmuladd  9676  modqmuladdnn0  9678  modqm1p1mod0  9685  modqmul1  9687  modfzo0difsn  9705  addmodlteq  9708  frec2uzzd  9710  frec2uzsucd  9711  frec2uzrand  9715  frecuzrdgrrn  9718  frec2uzrdg  9719  frecuzrdgrcl  9720  frecuzrdgsuc  9724  frecuzrdgrclt  9725  frecuzrdgg  9726  frecuzrdgdom  9728  frecuzrdgfun  9730  frecuzrdgsuctlem  9733  frecuzrdgsuct  9734  uzsinds  9751  iseqval  9763  iseqvalcbv  9764  iseqvalt  9765  iseqfclt  9769  iseqp1  9771  iseqp1t  9772  iseqoveq  9773  iseqss  9774  iseqsst  9775  iseqfveq2  9777  iseqshft2  9781  monoord  9784  monoord2  9785  iseqsplit  9787  iseqcaopr3  9789  iseqcaopr2  9790  iseqid2  9797  iseqhomo  9798  iseqz  9799  iseqdistr  9800  m1expcl2  9828  mulexp  9845  expadd  9848  expmul  9851  sq0i  9897  sqoddm1div8  9955  facp1  9987  faclbnd  9998  faclbnd3  10000  bcval  10006  bcn1  10015  ibcval5  10020  bcpasc  10023  bccl  10024  hashfz1  10040  omgadd  10059  hashfzo  10079  hashfzp1  10081  hashxp  10083  shftlem  10092  shftfvalg  10094  shftfibg  10096  shftfval  10097  shftfib  10099  shftfn  10100  shftf  10106  2shfti  10107  shftvalg  10112  shftval4g  10113  cjval  10120  imval  10125  cjexp  10168  cnrecnv  10185  cvg1nlemcau  10258  cvg1nlemres  10259  resqrexlemcalc3  10290  resqrexlemex  10299  rsqrmo  10301  resqrtcl  10303  rersqrtthlem  10304  sqrtsq  10318  absexp  10353  recan  10383  climshft  10531  climcn1  10535  climcn2  10536  subcn2  10538  serif0  10577  dvdsval2  10593  dvds0lem  10600  dvds1lem  10601  dvds2lem  10602  dvdsmulc  10618  divconjdvds  10644  odd2np1lem  10666  odd2np1  10667  ltoddhalfle  10687  halfleoddlt  10688  nn0o1gt2  10699  nn0o  10701  divalglemnn  10712  divalglemeunn  10715  divalglemex  10716  divalglemeuneg  10717  flodddiv4  10728  gcdabs1  10774  gcddiv  10802  dvdssqim  10807  rpmulgcd  10809  bezoutr1  10816  dvdslcm  10845  lcmeq0  10847  lcmdvds  10855  divgcdcoprm0  10877  prmind2  10896  isprm6  10920  rpexp  10926  sqrt2irr  10935  pw2dvdslemn  10937  pw2dvdseu  10940  oddpwdclemxy  10941  nn0gcdsq  10972  phicl2  10984  phibndlem  10986  hashdvds  10991  crth  10994  phimullem  10995  hashgcdlem  10997  qdencn  11271
  Copyright terms: Public domain W3C validator