Theorem opreq2 4890

Description: Equality theorem for operation value.

Assertion

Ref	Expression
opreq2	|- (A = B -> (CFA) = (CFB))

Proof of Theorem opreq2

Step	Hyp	Ref	Expression
1		opeq2 3159	. . 3 |- (A = B -> <.C, A>. = <.C, B>.)
2	1	fveq2d 4685	. 2 |- (A = B -> (F` <.C, A>.) = (F` <.C, B>.))
3		df-opr 4886	. 2 |- (CFA) = (F` <.C, A>.)
4		df-opr 4886	. 2 |- (CFB) = (F` <.C, B>.)
5	2, 3, 4	3eqtr4g 1953	1 |- (A = B -> (CFA) = (CFB))

Syntax hints:   -> wi 3   = wceq 1298  <.cop 3046  ` cfv 3998  (class class class)co 4884

This theorem is referenced by:  opreq12 4891  opreq2i 4893  opreq2d 4898  rcla4eopr 4915  foprcl 4944  ndmoprcl 4977  caoprcl 4985  caoprcom 4986  caoprass 4987  caoprcan 4988  caoprord 4989  caoprdistr 4992  caoprmo 5003  elrnoprabg 5066  curry1 5075  curry1val 5077  onopruni 5117  onopriun 5118  omv 5196  oev 5198  oesuc 5211  oacl 5215  omcl 5216  omclOLD 5217  oecl 5218  oeclOLD 5219  oa0r 5220  om0r 5221  om1r 5224  oe1m 5226  oaordi 5227  oaord 5228  oawordri 5232  oawordeulem 5236  oaass 5243  oarec 5244  omordi 5245  omord2 5246  omcan 5248  omwordri 5251  om00 5254  odi 5258  omass 5259  oen0 5261  oeordi 5262  oeord 5263  oecan 5264  oewordri 5267  oeworde 5268  oelim2 5270  oeoalem 5271  oeoa 5272  oeoelem 5273  oeoe 5274  nnacl 5281  nnaclOLD 5282  nnmcl 5283  nnmclOLD 5284  nnecl 5285  nneclOLD 5286  nnacom 5288  nnmsucr 5295  nnmsucrOLD 5296  nnmcom 5297  nnmcomOLD 5298  oaabs 5309  nneob 5312  th3qlem2 5374  th3q 5376  ecoprcom 5378  ecoprass 5379  ecoprdi 5380  map0 5403  unfilem2 5642  unfilem3 5643  cdaung 6071  cdaeng 6074  nnacda 6088  addcmpblnq 6204  addclpq 6210  mulclpq 6212  recmulpq 6222  dmrecpq 6226  ltapq 6228  ltmpq 6229  ltexpq 6232  ltbtwnpq 6236  ltrpq 6237  genpv 6254  genpass 6264  distrlem1pr 6279  1idpr 6285  prlem934 6291  ltexprlem3 6296  ltexprlem4 6297  ltexpri 6301  ltaprlem 6302  ltapr 6303  prlem936 6307  reclem3pr 6310  recexpr 6312  mulcmpblnrlem 6334  addclsr 6344  mulclsr 6345  ltasr 6361  negexsr 6363  recexsrlem 6364  mulgt0sr 6366  recexsr 6368  supsrlem2 6378  addcnsr 6405  mulcnsr 6406  axaddopr 6417  axmulopr 6418  axaddrcl 6425  axmulrcl 6427  axrnegex 6436  axrrecex 6437  axcnre 6439  pre-axltadd 6442  pre-axmulgt0 6443  cnegexlem1 6499  cnegex 6502  addcani 6505  addcaniOLD 6506  addcan 6507  negeui 6510  negeq 6514  subcl 6524  subaddi 6528  subadd 6532  negsub 6540  ine0 6597  1re 6598  mulneg1 6615  mul2negOLD 6619  negdi 6620  ltadd2i 6765  addge0iOLD 6778  add20i 6782  mulge0i 6787  msqge0i 6795  msqge0iOLD 6796  ltadd1 6806  leadd1 6808  ltsubadd 6810  lesubadd 6812  lt2add 6827  le2add 6828  addgt0OLD 6832  addgegt0OLD 6834  addge0OLD 6838  lesub0 6867  mulge0 6868  mulge0OLD 6869  recextlem2 6875  recex 6876  mulcani 6878  mulcant2i 6879  mul0ori 6882  mul0or 6884  receui 6890  divmuli 6894  divmulzi 6895  divmul 6896  divclzi 6900  divcl 6901  divcan1zi 6907  divcan2zi 6908  divcan1 6909  recne0zi 6914  recne0 6915  recid 6918  divreczi 6921  divrec 6922  divdirzi 6932  divdir 6933  divcan3 6938  div11 6941  recrec 6952  rec11ii 6953  rec11i 6954  redivcli 6976  redivclzi 6977  redivcl 6978  eqnegi 6982  ltmul1i 7000  ltdiv1i 7002  prodgt0 7004  prodge0 7006  ltmul1 7008  lemul1a 7019  lemul1aOLD 7020  ltdiv1 7031  ltdiv1OLD 7032  ltmuldiv 7045  ltmuldivOLD 7046  ltreci 7062  lt2msqi 7064  ltrec 7067  lerec 7068  nnaddcl 7123  nnmulcl 7124  nnsub 7141  nndiv 7143  2times 7188  nn0addcl 7329  nn0mulcli 7331  nn0mulcl 7332  nnnn0addcl 7334  nn0sub 7370  zdiv 7397  zq 7440  qreccl 7453  modval 7501  icoshftf1olem 7579  icoun 7582  snunioo 7584  uzaddcl 7618  fzrevral 7698  fzshftral 7701  fsequb 7702  cardfz 7719  seq1rn2 7734  ser1f 7741  shftfval 7755  seqzfveq 7797  seqzrn2 7799  dfseq0 7806  expp1 7817  expcllem 7818  1exp 7827  expeq0 7828  expne0i 7830  expgt0 7831  expge0 7833  expgt1 7834  expge1 7835  mulexp 7836  exprec 7837  exprecOLD 7838  expadd 7839  expmul 7840  expcan 7846  expwordi 7848  expmwordi 7851  exple1 7852  sqlecan 7887  binom2 7896  bernneq 7898  bernneqOLD 7899  expnbnd 7901  discrlem2 7907  discrlem 7909  nn0opth2 7918  sqrlem21 7943  sqrmuli 7955  sqr2irrlem5 7978  crui 7987  cru 7988  crne0i 7989  creur 7992  creui 7993  replim 8011  reim0b 8025  readd 8055  imadd 8058  cjadd 8062  cjmul 8063  cjexp 8067  abs00i 8093  absmul 8109  absdiv 8111  absexp 8119  cjdiv 8141  abssub 8146  abstri 8150  abs1mi 8156  recan 8157  abs3lem 8159  ser1absdiflem 8181  facdiv 8194  faclbnd3 8199  faclbnd4lem1 8200  faclbnd4lem2 8201  faclbnd4lem3 8202  faclbnd4lem4 8203  faclbnd6 8206  bcval 8210  bcpasc2 8220  bcpasci 8221  bcpasc 8222  bccl2 8223  clim 8237  fsump1slem 8272  fsumcllem 8274  fsum1ps 8278  fsumsplit 8280  fsumadd 8282  csbfsumlem 8286  fsumcom 8288  fsumrev 8289  fsumshft 8291  fsummulc1 8293  fsumconst 8298  fsumcmp 8300  fsumcmpndx2 8302  fsumabs 8303  binomlem1 8326  binomlem2 8327  binomlem3 8328  binomlem4 8329  binomlem6 8331  binomi 8332  bcxmaslem1 8334  bcxmas 8336  cvgcmp3cetlem1 8449  cvgcmp3cetlem2 8450  infcvgi 8485  expcnvlem3 8490  explecnv 8495  geoseri 8496  geolimilem 8497  geolim 8499  geolim1i 8500  geolim1 8501  cvgratlem1ALT 8509  cvgratlem2ALT 8510  cvgratlem1 8512  cvgratlem5 8516  fsum0diaglem2 8519  fsum0diag 8520  fsum0diag2 8521  fsum0diag4 8523  mulc1cncf 8541  ivthlem6 8548  ivthlem7 8549  efcltlem1 8566  dfef2i 8569  ef0lem 8572  efcl 8574  efcvg 8576  eftval 8578  erelem2 8582  erelem3 8583  erelem6 8586  efaddlem6 8605  efaddlem24 8623  efaddlem26 8625  efaddlem27 8626  efadd 8629  efexp 8634  ef1tllem 8643  ef01tlubi 8648  absef01tlubi 8650  eirr 8656  ef4p 8665  eflegeolem2 8679  eflegeo 8681  efm1legeo 8683  efcnlem4 8687  sinval 8694  cosval 8695  sinadd 8718  cosadd 8719  absef 8749  demoivre 8752  acdc2lem1 8757  acdc5lem1 8760  infpnlem2 8776  ruclem4 8782  ruclem32 8810  infmap2 8850  retopbas 8925  meteq0 9089  mettri2 9090  mettri4 9091  elbl 9115  blelrn 9125  blss 9130  ssblex 9133  blnei 9156  metcnp 9165  blssioo 9191  tgioolem 9192  lmbr 9206  fsumcnlem 9267  bcthlem15 9291  bcthlem17 9293  isgrp 9321  grpass 9327  grpidinvlem1 9328  grpidinvlem3 9330  grpidinvlem4 9331  grpidinv 9332  grpideu 9333  grpsn 9340  grpidinv2 9344  grprcan 9347  grpinvval 9351  grpinv 9353  grpinvid1 9356  grplcan 9359  isgrp2i 9360  gxnn0neg 9386  gxnn0suc 9387  gxcl 9388  gxcom 9392  gxinv 9393  gxid 9396  gxnn0add 9397  gxnn0mul 9400  grplactval 9405  grplactf1o 9406  ablcom 9411  gxdi 9422  issubgilem 9430  ablsn 9433  ghgrpilem1 9441  ghgrpilem3 9443  ghgrpilem4 9444  ghgrpi 9445  gagrpid 9458  gaass 9459  gacan 9460  ringid 9469  ringideu 9470  ringdi 9471  ringdir 9472  ringass 9473  cnring 9489  ringsn 9490  vcid 9502  vcdi 9503  vcdir 9504  vcass 9505  nvmul0or 9604  nvs 9622  nvtri 9630  sm1cnilem 9686  ipval 9692  lnolin 9754  bloval 9781  nmlno0 9795  blocnilem 9804  phpar2 9823  phpar 9824  ipdiri 9830  ipassi 9842  siilem1 9852  siii 9854  sii 9855  ip2eqi 9858  ajfun 9862  minveclem13 9902  minvecex 9923  minveceu 9928  minvecdist 9930  minveclem39 9932  htthlem2 9968  sincolem 10014  sineq0re 10067  efgh 10072  efghgrpilem 10073  efif 10075  efifo 10083  efif1lem6 10089  efif1 10091  shftefif1olem 10095  eff1i 10098  effoi 10099  ghomlin 10196  hmph 10241  subtopmet 10256  flimff 10317  opidon 10369  exidu1 10373  cmpidelt 10376  rngmgmbs4 10401  uznzr 10416  hvsubval 10518  hvmul0or 10526  hvsubsub4 10559  hvaddcani 10564  hvnegdi 10566  hvsubeq0 10567  hvaddcan 10569  hvsubadd 10577  hial0 10601  hial02 10602  hial2eq 10605  normlem6 10614  normlem9at 10620  normsub0 10636  norm-ii 10638  norm-iii 10640  normsub 10643  normpyth 10645  norm3dif 10650  norm3lemt 10652  norm3adifi 10653  normpar 10655  polid 10659  bcs 10681  hlimi 10689  hlim2 10693  shaddcl 10718  shaddclOLD 10719  shmulcl 10720  shmulclOLD 10721  hsn0elch 10753  ocsh 10789  ocorth 10797  ocin 10802  occllem2 10807  occllem7 10812  occllem8 10813  projlem1 10819  projlem7 10825  projlem17 10835  projlem20 10838  projlem22 10840  projlem26 10844  projlem28 10846  pjthlem13 10864  pjthlem14 10865  pjtheui 10868  omlsii 10878  pjoc1i 10897  shsel3 10912  shscli 10914  shscl 10915  choc0 10923  shslej 10983  shlub 10987  chlejb1 11068  chnle 11070  chjass 11089  ledi 11096  h1deoi 11105  h1de2i 11109  elspansn 11122  elspansn2 11123  spanunsni 11135  h1datomi 11137  pjoml6i 11165  cmbr3 11184  pjoml3 11188  osumlem5 11217  osumlem8 11220  osum 11223  spansncvi 11232  pjadji 11265  pjaddi 11266  pjsubi 11268  pjmuli 11269  pjcjt2 11272  hosubcl 11336  hoaddcom 11337  hoaddass 11345  hocsubdir 11348  ho0sub 11360  honegsub 11362  adjsym 11396  eigrei 11397  eigre 11398  eigposi 11399  eigorthi 11400  eigorth 11401  cnopc 11474  lnopl 11475  unop 11476  hmop 11483  cnfnc 11491  lnfnl 11492  adj1 11494  adjvalval 11498  braval 11504  kbval 11513  eleigvec 11518  hoddi 11552  lnopeq0lem2 11568  lnopunii 11574  lnophmi 11580  nmcopexlem4 11591  nmcopexi 11594  nmcfnexlem4 11620  nmcfnexi 11623  riesz3i 11632  riesz4i 11633  cnlnadjlem4 11640  cnlnadjlem5 11641  cnlnadji 11646  nmopadjlei 11658  nmopcoi 11665  cnvbraval 11681  leopg 11693  opsqrlem4 11714  hmopidmchi 11723  pjclem3 11770  hstel2 11791  stj 11807  mdbr 11866  dmdbr 11871  mdsl0 11882  chcv1 11927  chjatom 11929  cvexch 11946  atcvat4i 11969  sumdmdlem 11990  cdjreui 12004  cdj1i 12005  cdj3lem1 12006  cdj3lem2 12007  cdj3lem2b 12009  cdj3lem3b 12012  cdj3i 12013  fz1eqblem 13608  fz1eqb 13609  ghomgrpilem1 13628  elgiso 13639  cayleylem2 13642  cayleythlem 13645  nn0seqcvgd 13659  divides 13664  dvdscmul 13680  dvds2ln 13684  dvdstr 13687  dvdsle 13693  divalglem2 13698  divalglem4 13699  divalglem5 13700  divalglem9 13704  divalglem10 13705  divalg 13706  divalgmod 13709  ndvdssub 13710  gcddvds 13722  gcdcl 13724  gcd0id 13729  gcdaddmlem 13734  gcdaddm 13735  mulgcdlem6 13761  coprmdvds 13783  pw2eng 14419  iscst2 14520  iscst4 14522  labss1 14537  labss2 14539  jidd 14540  midd 14541  valvalcurfn 14554  nfwval 14588  sege 14595  geme2 14617  tolat 14631  fprodp1slem 14681  iscomb 14690  ridlideq 14695  rzrlzreq 14696  mgmlion 14697  smgrpass2 14701  clfsebs 14707  fincmpzer 14711  fprodadd 14713  isppm 14715  mndass2 14721  symgfo 14730  curgrpact 14735  grpdivone 14736  fprodneg 14741  prsubrtr 14763  ununr 14769  zerdivemp1 14785  rngridfz 14786  vecax5b 14802  vecax5c 14825  idtrgrp 14978  altretop 14997  cntrsetlem 14999  iintlem1 15010  iintlem2 15011  1ded 15085  domcmpd 15093  codcmpd 15094  cmpasso 15120  cmpida 15121  dualcat2lem 15129  dualded2lem 15130  dualcat2 15133  ismonb2 15161  cmpmon 15164  icmpmon 15165  idmon 15166  isepib 15169  cinvlem3 15178  reconn 15451  ivthALT 15454  rnelfm 15593  fmfnfm 15598  fcluscnplem 15617  fcluscnp 15618  fclusff 15623  eropreu 15733  eroprv 15734  add20 15777  divexp 15779  eluzadd 15782  eluzsub 15783  fzfi 15786  seq11g 15804  seq1p1g 15805  seqz1g 15806  seqzp1g 15807  seq1seqzg 15808  sdclem1 15809  sdclem2 15810  sdc 15811  fdc 15812  seq1eq2 15817  fsum00 15820  fsumlt 15821  fsumltisumi 15823  fsumltisum 15824  fsumleisumi 15826  fsumleisum 15827  iserzshft2 15829  isumshft2 15830  fsumlt1 15831  trirn 15834  mettrifi 15847  geomcau 15849  metdcn 15853  lincmb01icc 15879  sub2cncf 15886  txcnoprab 15911  txmet 15925  sstotbnd 15936  totbndss 15937  isbnd3 15941  blbnd 15943  totbndbnd 15944  ismtycnv 15949  ismtyhmeolem 15950  ismtyhmeo 15951  ismtybndlem 15952  ismtyres 15954  heiborlem16 15970  heiborlem23 15977  heiborlem25 15979  heiborlem26 15980  heiborlem28 15982  heiborlem29 15983  heiborlem30 15984  heiborlem32 15986  heiborlem35 15989  bfplem5 16002  bfplem8 16005  bfplem9 16006  bfplem11 16008  recms 16010  rrnval 16013  iccbnd 16026  exidres 16031  exidresid 16032  ghomco 16040  phtpyfval 16046  phtpycom 16050  phtpycolem1 16051  phtpycolem2 16052  phtpycolem3 16053  phtpycolem4 16054  phtpyco 16056  phtpcval 16058  isphtpc 16059  reparphtlem1 16063  reparphtlem2 16064  reparpht 16065  pcofval 16072  pcoval1 16074  pcoval2 16075  pcocn 16076  pcohtpylem1 16080  pcohtpylem2 16081  pcohtpylem3 16082  pcohtpy 16083  pcopt 16084  pcoass 16085  pcorevlem 16086  pcorev 16087  pi1bval 16088  pi1fval 16092  pi1gp 16095  isringd 16097  zerdivemp1x 16108  isdivrng2 16111  rnghomadd 16123  rnghommul 16124  rngisoval 16131  isriscg 16138  iscringd 16147  crngcom 16149  idladdcl 16167  idllmulcl 16168  idlrmulcl 16169  0idl 16173  divrngidl 16176  keridl 16180  smprngpr 16200  prnc 16215  pridlc 16219  dmnnzd 16223  dfstruct2 16709  fnelstr 16717  strdif 16719  latlem 16850  cmtval 16938  omllaw3 16966  cmtbr3 16975  hlsuprexch 17033  atcvr0eq 17064  cvrat4 17076  grplem1 17105  grpidinvlem1NEW 17109  grpidinvlem3NEW 17111  grpidinvlem4NEW 17112  grpidinvNEW 17113  grpideuNEW 17114  grpidinv2NEW 17119  grprcanNEW 17122  grpinvvalNEW 17126  grpinvNEW 17128  grpinvid1NEW 17131  grplcanNEW 17134  ablcomNEW 17138  ringiNEW 17143  ringideuNEW 17146  ringidmlemNEW 17153  islinei 17221  psubspi2 17229  elpaddn0 17261  elpaddri 17263  elpaddat 17265  paddasslem17 17297  pmodlem2 17308  pmapjat 17314

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-xp 4000  df-cnv 4002  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fv 4014  df-opr 4886

Copyright terms: Public domain