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

Theorem oveq1 5547
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 3577 . . 3  |-  ( A  =  B  ->  <. A ,  C >.  =  <. B ,  C >. )
21fveq2d 5210 . 2  |-  ( A  =  B  ->  ( F `  <. A ,  C >. )  =  ( F `  <. B ,  C >. ) )
3 df-ov 5543 . 2  |-  ( A F C )  =  ( F `  <. A ,  C >. )
4 df-ov 5543 . 2  |-  ( B F C )  =  ( F `  <. B ,  C >. )
52, 3, 43eqtr4g 2113 1  |-  ( A  =  B  ->  ( A F C )  =  ( B F C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1259   <.cop 3406   ` cfv 4930  (class class class)co 5540
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-rex 2329  df-v 2576  df-un 2950  df-sn 3409  df-pr 3410  df-op 3412  df-uni 3609  df-br 3793  df-iota 4895  df-fv 4938  df-ov 5543
This theorem is referenced by:  oveq12  5549  oveq1i  5550  oveq1d  5555  rspceov  5575  fovcl  5634  ovmpt2s  5652  ov2gf  5653  ovi3  5665  caovclg  5681  caovcomg  5684  caovassg  5687  caovcang  5690  caovcan  5693  caovordig  5694  caovordg  5696  caovord  5700  caovdig  5703  caovdirg  5706  caovimo  5722  grpridd  5725  suppssov1  5737  off  5752  omcl  6072  oeicl  6073  omv2  6076  nnm0r  6089  nnacom  6094  nndi  6096  nnmass  6097  nnmsucr  6098  nnmcom  6099  nnaword  6115  nnmord  6121  nnm00  6133  eroveu  6228  th3qlem2  6240  th3q  6242  ecovcom  6244  ecovicom  6245  ecovass  6246  ecoviass  6247  ecovdi  6248  ecovidi  6249  addcmpblnq  6523  addclnq  6531  mulclnq  6532  mulidnq  6545  recexnq  6546  recmulnqg  6547  ltanqg  6556  ltmnqg  6557  ltexnqq  6564  enq0ref  6589  enq0tr  6590  addcmpblnq0  6599  mulnnnq0  6606  addclnq0  6607  mulclnq0  6608  distrnq0  6615  mulcomnq0  6616  addassnq0  6618  prarloclemlo  6650  prarloclem3  6653  prarloclem5  6656  prarloclemcalc  6658  genipv  6665  genpassl  6680  genpassu  6681  addlocprlemeq  6689  distrlem4prl  6740  distrlem4pru  6741  ltexprlemdisj  6762  ltexprlemloc  6763  ltexprlemrl  6766  ltexprlemru  6768  prplnqu  6776  cauappcvgprlemm  6801  cauappcvgprlemopl  6802  cauappcvgprlemlol  6803  cauappcvgprlemdisj  6807  cauappcvgprlemloc  6808  cauappcvgprlemladdfl  6811  cauappcvgprlemladdru  6812  cauappcvgprlemladdrl  6813  cauappcvgprlem1  6815  cauappcvgprlemlim  6817  cauappcvgpr  6818  caucvgprlemm  6824  caucvgprlemopl  6825  caucvgprlemlol  6826  caucvgprlemdisj  6830  caucvgprlemloc  6831  caucvgprlemladdrl  6834  caucvgprlem1  6835  caucvgpr  6838  caucvgprprlemell  6841  caucvgprprlemml  6850  caucvgprpr  6868  mulcmpblnrlemg  6883  addclsr  6896  mulclsr  6897  0idsr  6910  1idsr  6911  00sr  6912  ltasrg  6913  recexgt0sr  6916  mulgt0sr  6920  mulextsr1  6923  prsrriota  6930  caucvgsrlemgt1  6937  caucvgsrlemoffres  6942  pitonn  6982  peano2nnnn  6987  axaddrcl  6999  axmulrcl  7001  axaddcom  7002  ax1rid  7009  ax0id  7010  axprecex  7012  axcnre  7013  axpre-ltadd  7018  axpre-mulgt0  7019  axpre-mulext  7020  rereceu  7021  peano5nnnn  7024  axcaucvglemcau  7030  axcaucvglemres  7031  mulid1  7082  cnegexlem1  7249  cnegexlem2  7250  cnegex  7252  addcan2  7255  subval  7266  addlsub  7440  apreim  7668  recexap  7708  receuap  7724  divvalap  7727  cju  7989  peano2nn  8002  nn1m1nn  8008  nn1suc  8009  nnsub  8028  nnm1nn0  8280  zdiv  8386  zneo  8398  nneoor  8399  zeo  8402  peano5uzti  8405  nn0ind-raph  8414  uzind4s  8629  uzind4s2  8630  qmulz  8655  cnref1o  8680  nn0ledivnn  8785  fzsuc2  9043  fzm1  9064  fzoval  9107  qbtwnzlemstep  9205  qbtwnzlemshrink  9206  qbtwnzlemex  9207  qbtwnz  9208  rebtwn2zlemstep  9209  rebtwn2zlemshrink  9210  rebtwn2z  9211  flqlelt  9226  flqbi  9240  fldiv4p1lem1div2  9255  modqval  9274  modqadd1  9311  modqmuladd  9316  modqmuladdnn0  9318  modqm1p1mod0  9325  modqmul1  9327  modfzo0difsn  9345  addmodlteq  9348  frec2uzzd  9350  frec2uzsucd  9351  frec2uzrand  9355  frecuzrdgrrn  9358  frec2uzrdg  9359  frecuzrdgsuc  9365  iseqval  9384  iseqp1  9389  iseqss  9390  iseqfveq2  9392  iseqshft2  9396  monoord  9399  monoord2  9400  iseqsplit  9402  iseqcaopr3  9404  iseqcaopr2  9405  iseqhomo  9412  iseqz  9413  iseqdistr  9414  m1expcl2  9442  mulexp  9459  expadd  9462  expmul  9465  sq0i  9511  sqoddm1div8  9569  facp1  9598  faclbnd  9609  faclbnd3  9611  bcval  9617  bcn1  9626  ibcval5  9631  bcpasc  9634  bccl  9635  shftlem  9645  shftfvalg  9647  shftfibg  9649  shftfval  9650  shftfib  9652  shftfn  9653  shftf  9659  2shfti  9660  shftvalg  9665  shftval4g  9666  cjval  9673  imval  9678  cjexp  9721  cnrecnv  9738  cvg1nlemcau  9811  cvg1nlemres  9812  resqrexlemcalc3  9843  resqrexlemex  9852  rsqrmo  9854  resqrtcl  9856  rersqrtthlem  9857  sqrtsq  9871  absexp  9906  recan  9936  climshft  10056  climcn1  10060  climcn2  10061  subcn2  10063  serif0  10102  dvdsval2  10111  dvds0lem  10118  dvds1lem  10119  dvds2lem  10120  dvdsmulc  10135  divconjdvds  10161  odd2np1lem  10183  odd2np1  10184  ltoddhalfle  10205  halfleoddlt  10206  nn0o1gt2  10217  nn0o  10219  divalglemnn  10230  divalglemeunn  10233  divalglemex  10234  divalglemeuneg  10235  flodddiv4  10246  sqrt2irr  10251  pw2dvdslemn  10253  pw2dvdseu  10256  oddpwdclemxy  10257  qdencn  10511
  Copyright terms: Public domain W3C validator