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

Theorem oveq1 5497
Description: Equality theorem for operation value. (Contributed by NM, 28-Feb-1995.)
Assertion
Ref Expression
oveq1  |-  ( A  =  B  ->  ( A F C )  =  ( B F C ) )

Proof of Theorem oveq1
StepHypRef Expression
1 opeq1 3546 . . 3  |-  ( A  =  B  ->  <. A ,  C >.  =  <. B ,  C >. )
21fveq2d 5160 . 2  |-  ( A  =  B  ->  ( F `  <. A ,  C >. )  =  ( F `  <. B ,  C >. ) )
3 df-ov 5493 . 2  |-  ( A F C )  =  ( F `  <. A ,  C >. )
4 df-ov 5493 . 2  |-  ( B F C )  =  ( F `  <. B ,  C >. )
52, 3, 43eqtr4g 2097 1  |-  ( A  =  B  ->  ( A F C )  =  ( B F C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1243   <.cop 3375   ` cfv 4880  (class class class)co 5490
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 2309  df-v 2556  df-un 2919  df-sn 3378  df-pr 3379  df-op 3381  df-uni 3578  df-br 3762  df-iota 4845  df-fv 4888  df-ov 5493
This theorem is referenced by:  oveq12  5499  oveq1i  5500  oveq1d  5505  rspceov  5525  fovcl  5584  ovmpt2s  5602  ov2gf  5603  ovi3  5615  caovclg  5631  caovcomg  5634  caovassg  5637  caovcang  5640  caovcan  5643  caovordig  5644  caovordg  5646  caovord  5650  caovdig  5653  caovdirg  5656  caovimo  5672  grpridd  5675  suppssov1  5687  off  5702  omcl  6019  oeicl  6020  omv2  6023  nnm0r  6036  nnacom  6041  nndi  6043  nnmass  6044  nnmsucr  6045  nnmcom  6046  nnaword  6062  nnmord  6068  nnm00  6080  eroveu  6175  th3qlem2  6187  th3q  6189  ecovcom  6191  ecovicom  6192  ecovass  6193  ecoviass  6194  ecovdi  6195  ecovidi  6196  addcmpblnq  6437  addclnq  6445  mulclnq  6446  mulidnq  6459  recexnq  6460  recmulnqg  6461  ltanqg  6470  ltmnqg  6471  ltexnqq  6478  enq0ref  6503  enq0tr  6504  addcmpblnq0  6513  mulnnnq0  6520  addclnq0  6521  mulclnq0  6522  distrnq0  6529  mulcomnq0  6530  addassnq0  6532  prarloclemlo  6564  prarloclem3  6567  prarloclem5  6570  prarloclemcalc  6572  genipv  6579  genpassl  6594  genpassu  6595  addlocprlemeq  6603  distrlem4prl  6654  distrlem4pru  6655  ltexprlemdisj  6676  ltexprlemloc  6677  ltexprlemrl  6680  ltexprlemru  6682  prplnqu  6690  cauappcvgprlemm  6715  cauappcvgprlemopl  6716  cauappcvgprlemlol  6717  cauappcvgprlemdisj  6721  cauappcvgprlemloc  6722  cauappcvgprlemladdfl  6725  cauappcvgprlemladdru  6726  cauappcvgprlemladdrl  6727  cauappcvgprlem1  6729  cauappcvgprlemlim  6731  cauappcvgpr  6732  caucvgprlemm  6738  caucvgprlemopl  6739  caucvgprlemlol  6740  caucvgprlemdisj  6744  caucvgprlemloc  6745  caucvgprlemladdrl  6748  caucvgprlem1  6749  caucvgpr  6752  caucvgprprlemell  6755  caucvgprprlemml  6764  caucvgprpr  6782  mulcmpblnrlemg  6797  addclsr  6810  mulclsr  6811  0idsr  6824  1idsr  6825  00sr  6826  ltasrg  6827  recexgt0sr  6830  mulgt0sr  6834  mulextsr1  6837  prsrriota  6844  caucvgsrlemgt1  6851  caucvgsrlemoffres  6856  pitonn  6896  peano2nnnn  6901  axaddrcl  6913  axmulrcl  6915  axaddcom  6916  ax1rid  6923  ax0id  6924  axprecex  6926  axcnre  6927  axpre-ltadd  6932  axpre-mulgt0  6933  axpre-mulext  6934  rereceu  6935  peano5nnnn  6938  axcaucvglemcau  6944  axcaucvglemres  6945  mulid1  6996  cnegexlem1  7157  cnegexlem2  7158  cnegex  7160  addcan2  7163  subval  7174  apreim  7561  recexap  7601  receuap  7617  divvalap  7620  cju  7880  peano2nn  7893  nn1m1nn  7899  nn1suc  7900  nnsub  7919  nnm1nn0  8186  zdiv  8291  zneo  8302  nneoor  8303  zeo  8306  peano5uzti  8309  nn0ind-raph  8318  uzind4s  8496  uzind4s2  8497  qmulz  8521  cnref1o  8544  fzsuc2  8899  fzm1  8920  fzoval  8963  frec2uzzd  9055  frec2uzsucd  9056  frec2uzrand  9060  frecuzrdgrrn  9063  frec2uzrdg  9064  frecuzrdgsuc  9070  iseqval  9089  iseqp1  9094  iseqss  9095  iseqfveq2  9097  iseqshft2  9101  monoord  9104  monoord2  9105  iseqsplit  9107  iseqcaopr3  9109  iseqcaopr2  9110  iseqhomo  9117  iseqdistr  9118  m1expcl2  9146  mulexp  9163  expadd  9166  expmul  9169  sq0i  9214  shftlem  9286  shftfvalg  9288  shftfibg  9290  shftfval  9291  shftfib  9293  shftfn  9294  shftf  9300  2shfti  9301  shftvalg  9306  shftval4g  9307  cjval  9314  imval  9319  cjexp  9362  cnrecnv  9379  cvg1nlemcau  9452  cvg1nlemres  9453  resqrexlemcalc3  9483  resqrexlemex  9492  rsqrmo  9494  resqrtcl  9496  rersqrtthlem  9497  sqrtsq  9511  absexp  9544  recan  9574  climshft  9693  climcn1  9697  climcn2  9698  subcn2  9700  serif0  9739  sqrt2irr  9746
  Copyright terms: Public domain W3C validator