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-bndl 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  6416  enq0tr  6417  addcmpblnq0  6426  mulnnnq0  6433  addclnq0  6434  mulclnq0  6435  distrnq0  6442  mulcomnq0  6443  addassnq0  6445  prarloclemlo  6477  prarloclem3  6480  prarloclem5  6483  prarloclemcalc  6485  genipv  6492  genpassl  6507  genpassu  6508  addlocprlemeq  6516  distrlem4prl  6560  distrlem4pru  6561  ltexprlemdisj  6580  ltexprlemloc  6581  ltexprlemrl  6584  ltexprlemru  6586  cauappcvgprlemm  6617  cauappcvgprlemopl  6618  cauappcvgprlemlol  6619  cauappcvgprlemdisj  6623  cauappcvgprlemloc  6624  cauappcvgprlemladdfl  6627  cauappcvgprlemladdru  6628  cauappcvgprlemladdrl  6629  cauappcvgprlem1  6631  cauappcvgprlemlim  6633  cauappcvgpr  6634  caucvgprlemm  6639  caucvgprlemopl  6640  caucvgprlemlol  6641  caucvgprlemdisj  6645  caucvgprlemloc  6646  caucvgprlemladdrl  6649  caucvgprlem1  6650  caucvgpr  6653  mulcmpblnrlemg  6668  addclsr  6681  mulclsr  6682  0idsr  6695  1idsr  6696  00sr  6697  ltasrg  6698  recexgt0sr  6701  mulgt0sr  6704  mulextsr1  6707  pitonn  6744  axaddrcl  6751  axmulrcl  6753  axaddcom  6754  ax1rid  6761  ax0id  6762  axprecex  6764  axcnre  6765  axpre-ltadd  6770  axpre-mulgt0  6771  axpre-mulext  6772  mulid1  6822  cnegexlem1  6983  cnegexlem2  6984  cnegex  6986  addcan2  6989  subval  7000  apreim  7387  recexap  7416  receuap  7432  divvalap  7435  cju  7694  peano2nn  7707  nn1m1nn  7713  nn1suc  7714  nnsub  7733  nnm1nn0  7999  zdiv  8104  zneo  8115  nneoor  8116  zeo  8119  peano5uzti  8122  nn0ind-raph  8131  uzind4s  8309  uzind4s2  8310  qmulz  8334  cnref1o  8357  fzsuc2  8711  fzm1  8732  fzoval  8775  frec2uzzd  8867  frec2uzsucd  8868  frec2uzrand  8872  frecuzrdgrrn  8875  frec2uzrdg  8876  frecuzrdgsuc  8882  iseqval  8900  iseqp1  8904  iseqfveq2  8905  m1expcl2  8931  mulexp  8948  expadd  8951  expmul  8954  sq0i  8998  cjval  9073  imval  9078  cjexp  9121  cnrecnv  9138  sqrtsq  9214
  Copyright terms: Public domain W3C validator