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

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

Proof of Theorem oveq1
StepHypRef Expression
1 opeq1 3540 . . 3 (A = B → ⟨A, 𝐶⟩ = ⟨B, 𝐶⟩)
21fveq2d 5125 . 2 (A = B → (𝐹‘⟨A, 𝐶⟩) = (𝐹‘⟨B, 𝐶⟩))
3 df-ov 5458 . 2 (A𝐹𝐶) = (𝐹‘⟨A, 𝐶⟩)
4 df-ov 5458 . 2 (B𝐹𝐶) = (𝐹‘⟨B, 𝐶⟩)
52, 3, 43eqtr4g 2094 1 (A = B → (A𝐹𝐶) = (B𝐹𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1242  cop 3370  cfv 4845  (class class class)co 5455
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 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-rex 2306  df-v 2553  df-un 2916  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-iota 4810  df-fv 4853  df-ov 5458
This theorem is referenced by:  oveq12  5464  oveq1i  5465  oveq1d  5470  rspceov  5489  fovcl  5548  ovmpt2s  5566  ov2gf  5567  ovi3  5579  caovclg  5595  caovcomg  5598  caovassg  5601  caovcang  5604  caovcan  5607  caovordig  5608  caovordg  5610  caovord  5614  caovdig  5617  caovdirg  5620  caovimo  5636  grpridd  5639  suppssov1  5651  off  5666  omcl  5980  oeicl  5981  omv2  5984  nnm0r  5997  nnacom  6002  nndi  6004  nnmass  6005  nnmsucr  6006  nnmcom  6007  nnaword  6020  nnmord  6026  nnm00  6038  eroveu  6133  th3qlem2  6145  th3q  6147  ecovcom  6149  ecovicom  6150  ecovass  6151  ecoviass  6152  ecovdi  6153  ecovidi  6154  addcmpblnq  6351  addclnq  6359  mulclnq  6360  mulidnq  6373  recexnq  6374  recmulnqg  6375  ltanqg  6384  ltmnqg  6385  ltexnqq  6391  enq0ref  6415  enq0tr  6416  addcmpblnq0  6425  mulnnnq0  6432  addclnq0  6433  mulclnq0  6434  distrnq0  6441  mulcomnq0  6442  addassnq0  6444  prarloclemlo  6476  prarloclem3  6479  prarloclem5  6482  prarloclemcalc  6484  genipv  6491  genpassl  6506  genpassu  6507  addlocprlemeq  6515  distrlem4prl  6559  distrlem4pru  6560  ltexprlemdisj  6579  ltexprlemloc  6580  ltexprlemrl  6583  ltexprlemru  6585  cauappcvgprlemm  6616  cauappcvgprlemopl  6617  cauappcvgprlemlol  6618  cauappcvgprlemdisj  6622  cauappcvgprlemloc  6623  cauappcvgprlemladdfl  6626  cauappcvgprlemladdru  6627  cauappcvgprlemladdrl  6628  cauappcvgprlem1  6630  cauappcvgprlemlim  6632  cauappcvgpr  6633  mulcmpblnrlemg  6648  addclsr  6661  mulclsr  6662  0idsr  6675  1idsr  6676  00sr  6677  ltasrg  6678  recexgt0sr  6681  mulgt0sr  6684  mulextsr1  6687  pitonn  6724  axaddrcl  6731  axmulrcl  6733  axaddcom  6734  ax1rid  6741  ax0id  6742  axprecex  6744  axcnre  6745  axpre-ltadd  6750  axpre-mulgt0  6751  axpre-mulext  6752  mulid1  6802  cnegexlem1  6963  cnegexlem2  6964  cnegex  6966  addcan2  6969  subval  6980  apreim  7367  recexap  7396  receuap  7412  divvalap  7415  cju  7674  peano2nn  7687  nn1m1nn  7693  nn1suc  7694  nnsub  7713  nnm1nn0  7979  zdiv  8084  zneo  8095  nneoor  8096  zeo  8099  peano5uzti  8102  nn0ind-raph  8111  uzind4s  8289  uzind4s2  8290  qmulz  8314  cnref1o  8337  fzsuc2  8691  fzm1  8712  fzoval  8755  frec2uzzd  8847  frec2uzsucd  8848  frec2uzrand  8852  frecuzrdgrrn  8855  frec2uzrdg  8856  frecuzrdgsuc  8862  iseqval  8880  iseqp1  8884  iseqfveq2  8885  m1expcl2  8911  mulexp  8928  expadd  8931  expmul  8934  sq0i  8978  cjval  9053  imval  9058  cjexp  9101  cnrecnv  9118  sqrtsq  9194
  Copyright terms: Public domain W3C validator