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

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

Proof of Theorem oveq2
StepHypRef Expression
1 opeq2 3550 . . 3  |-  ( A  =  B  ->  <. C ,  A >.  =  <. C ,  B >. )
21fveq2d 5182 . 2  |-  ( A  =  B  ->  ( F `  <. C ,  A >. )  =  ( F `  <. C ,  B >. ) )
3 df-ov 5515 . 2  |-  ( C F A )  =  ( F `  <. C ,  A >. )
4 df-ov 5515 . 2  |-  ( C F B )  =  ( F `  <. C ,  B >. )
52, 3, 43eqtr4g 2097 1  |-  ( A  =  B  ->  ( C F A )  =  ( C F B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1243   <.cop 3378   ` cfv 4902  (class class class)co 5512
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 2312  df-v 2559  df-un 2922  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-br 3765  df-iota 4867  df-fv 4910  df-ov 5515
This theorem is referenced by:  oveq12  5521  oveq2i  5523  oveq2d  5528  rspceov  5547  fovcl  5606  ovmpt2s  5624  ov2gf  5625  ovi3  5637  caovclg  5653  caovcomg  5656  caovassg  5659  caovcang  5662  caovcan  5665  caovordig  5666  caovordg  5668  caovord  5672  caovdig  5675  caovdirg  5678  caovimo  5694  grprinvlem  5695  grprinvd  5696  suppssov1  5709  off  5724  omv  6035  oeiv  6036  oasuc  6044  omsuc  6051  nna0r  6057  nnm0r  6058  nnacl  6059  nnmcl  6060  nnacom  6063  nnaass  6064  nndi  6065  nnmass  6066  nnmsucr  6067  nnmcom  6068  nnaordi  6081  nnaord  6082  nnmordi  6089  nnmord  6090  nnaordex  6100  nnawordex  6101  nnm00  6102  eroveu  6197  ecopovtrn  6203  ecopovtrng  6206  th3qlem2  6209  th3q  6211  ecovcom  6213  ecovicom  6214  ecovass  6215  ecoviass  6216  ecovdi  6217  ecovidi  6218  addcanpig  6430  mulcanpig  6431  addcmpblnq  6463  addclnq  6471  mulclnq  6472  recexnq  6486  recmulnqg  6487  ltanqg  6496  ltmnqg  6497  ltexnqq  6504  enq0ref  6529  enq0tr  6530  addcmpblnq0  6539  mulnnnq0  6546  addclnq0  6547  mulclnq0  6548  distrnq0  6555  mulcomnq0  6556  addassnq0  6558  nq02m  6561  prarloclem3  6593  genipv  6605  genpassl  6620  genpassu  6621  addlocpr  6632  distrlem1prl  6678  distrlem1pru  6679  1idprl  6686  1idpru  6687  ltexprlemell  6694  ltexprlemelu  6695  ltexpri  6709  lteupri  6713  ltaprlem  6714  recexprlem1ssl  6729  recexprlem1ssu  6730  recexpr  6734  cauappcvgprlemm  6741  cauappcvgprlemdisj  6747  cauappcvgprlemloc  6748  cauappcvgprlemladdru  6752  cauappcvgprlemladdrl  6753  cauappcvgprlem1  6755  cauappcvgprlemlim  6757  cauappcvgpr  6758  mulcmpblnrlemg  6823  addclsr  6836  mulclsr  6837  ltasrg  6853  negexsr  6855  recexgt0sr  6856  mulgt0sr  6860  mulextsr1  6863  srpospr  6865  caucvgsrlemgt1  6877  axaddrcl  6939  axmulrcl  6941  axaddcom  6942  axrnegex  6951  axprecex  6952  axcnre  6953  axpre-ltadd  6958  axpre-mulgt0  6959  axpre-mulext  6960  rereceu  6961  recriota  6962  axcaucvglemres  6971  readdcan  7151  cnegexlem1  7184  cnegex  7187  addcan  7189  negeq  7202  subadd  7212  ine0  7389  rimul  7574  cru  7591  apreim  7592  recexap  7632  mulcanapd  7640  receuap  7648  divmulap  7652  cju  7911  nnaddcl  7932  nnmulcl  7933  nnsub  7950  nnnn0addcl  8210  zaddcllempos  8280  zaddcl  8283  zdiv  8326  deceq1  8368  deceq2  8369  uzaddcl  8527  zq  8559  qreccl  8574  cnref1o  8580  fzsuc2  8939  fzrevral  8965  fzshftral  8968  2ffzeq  8996  qbtwnzlemshrink  9102  rebtwn2zlemshrink  9106  frecuzrdgrrn  9168  frec2uzrdg  9169  frecuzrdgsuc  9175  frecfzennn  9177  iseqcaopr3  9214  iseqcaopr2  9215  iseqid  9221  iseqhomo  9222  iseqdistr  9223  expp1  9236  expnegap0  9237  expcllem  9240  expcl2lemap  9241  m1expcl2  9251  expap0  9259  mulexp  9268  expadd  9271  expmul  9274  leexp2r  9282  leexp1a  9283  bernneq  9343  expnbnd  9346  shftfvalg  9393  shftfval  9396  cjth  9420  remim  9434  reim0b  9436  cjexp  9467  cnrecnv  9484  cvg1nlemcau  9557  cvg1nlemres  9558  recvguniq  9567  resqrexlemp1rp  9578  resqrexlemfp1  9581  resqrexlemlo  9585  resqrexlemgt0  9592  resqrexlemoverl  9593  resqrexlemglsq  9594  resqrexlemsqa  9596  resqrexlemex  9597  resqrex  9598  absexp  9649  recan  9679  climcn2  9804  subcn2  9806  sqrt2irr  9852  nn0seqcvgd  9854
  Copyright terms: Public domain W3C validator